fix: use withMainContext in borelize tactic (#5237)

Also make it use `withoutRecover` when elaborating arguments (like in `apply`), and in addition use `exprToSyntax` to make sure each argument is elaborated only once.

Adding `withMainContext` fixes the bug reported by @urkud [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20.60borelize.60/near/367468010).

Author: kmill

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -220,17 +220,19 @@ Finally, `borelize α β γ` runs `borelize α; borelize β; borelize γ`.
 -/
 syntax "borelize" (ppSpace colGt term:max)* : tactic
 
-/-- Add instances `borel $t : MeasurableSpace $t` and `⟨rfl⟩ : BorelSpace $t`. -/
-def addBorelInstance (t : Term) : TacticM Unit := do
+/-- Add instances `borel e : MeasurableSpace e` and `⟨rfl⟩ : BorelSpace e`. -/
+def addBorelInstance (e : Expr) : TacticM Unit := do
+  let t ← Lean.Elab.Term.exprToSyntax e
   evalTactic <| ← `(tactic|
     refine_lift
       letI : MeasurableSpace $t := borel $t
       haveI : BorelSpace $t := ⟨rfl⟩
       ?_)
 
-/-- Given a type `$t`, an assumption `i : MeasurableSpace $t`, and an instance `[BorelSpace $t]`,
-replace `i` with `borel $t`. -/
-def borelToRefl (t : Term) (i : FVarId) : TacticM Unit := do
+/-- Given a type `e`, an assumption `i : MeasurableSpace e`, and an instance `[BorelSpace e]`,
+replace `i` with `borel e`. -/
+def borelToRefl (e : Expr) (i : FVarId) : TacticM Unit := do
+  let t ← Lean.Elab.Term.exprToSyntax e
   evalTactic <| ← `(tactic|
     have := @BorelSpace.measurable_eq $t _ _ _)
   liftMetaTactic fun m => return [← subst m i]
@@ -242,11 +244,11 @@ def borelToRefl (t : Term) (i : FVarId) : TacticM Unit := do
 /-- Given a type `$t`, if there is an assumption `[i : MeasurableSpace $t]`, then try to prove
 `[BorelSpace $t]` and replace `i` with `borel $t`. Otherwise, add instances
 `borel $t : MeasurableSpace $t` and `⟨rfl⟩ : BorelSpace $t`. -/
-def borelize (t : Term) : TacticM Unit := do
+def borelize (t : Term) : TacticM Unit := withMainContext <| do
   let u ← mkFreshLevelMVar
-  let e ← Tactic.elabTermEnsuringType t (mkSort (mkLevelSucc u))
+  let e ← withoutRecover <| Tactic.elabTermEnsuringType t (mkSort (mkLevelSucc u))
   let i? ← findLocalDeclWithType? (← mkAppOptM ``MeasurableSpace #[e])
-  i?.elim (addBorelInstance t) (borelToRefl t)
+  i?.elim (addBorelInstance e) (borelToRefl e)
 
 elab_rules : tactic
   | `(tactic| borelize $[$t:term]*) => t.forM borelize

test/borelize.lean

@@ -0,0 +1,35 @@
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+
+example [TopologicalSpace α] [inst : MeasurableSpace α] [BorelSpace α] : MeasurableSet (∅ : Set α) := by
+  guard_target = @MeasurableSet α inst ∅
+  borelize α
+  guard_target = @MeasurableSet α (borel α) ∅
+  apply MeasurableSet.empty
+
+example [TopologicalSpace α] : True := by
+  borelize α
+  have h : MeasurableSet (∅ : Set α) := MeasurableSet.empty
+  guard_hyp h : @MeasurableSet α (borel α) ∅
+  trivial
+
+example : True := by
+  obtain ⟨α, ⟨hα⟩⟩ : ∃ α : Type, Nonempty (TopologicalSpace α) := ⟨ℕ, ⟨inferInstance⟩⟩
+  borelize α
+  have h : MeasurableSet (∅ : Set α) := MeasurableSet.empty
+  guard_hyp h : @MeasurableSet α (borel α) ∅
+  trivial
+
+example : True := by
+  set α := ℕ
+  borelize α
+  have h : MeasurableSet (∅ : Set α) := MeasurableSet.empty
+  guard_hyp h : @MeasurableSet α (borel α) ∅
+  trivial
+
+example : True := by
+  have h1 : MeasurableSet (∅ : Set ℕ) := MeasurableSet.empty
+  guard_hyp h1 : @MeasurableSet ℕ Nat.instMeasurableSpace ∅
+  borelize ℕ
+  have h2 : MeasurableSet (∅ : Set ℕ) := MeasurableSet.empty
+  guard_hyp h2 : @MeasurableSet ℕ (borel ℕ) ∅
+  trivial