feat: instance for Inhabited (TacticM α) (#5401)

Provide an instance `Inhabited (TacticM α)`, even when `α` is not known
to be inhabited.

The default value is just the default value of `TermElabM α`, which
already has a similar instance.

src/Lean/Elab/Tactic/Basic.lean

@@ -49,6 +49,9 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
+instance : Inhabited (TacticM α) where
+  default := fun _ _ => default
+
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals