refactor: more readable error message when borelize fails (#7231)

`borelize X` fails when `‹TopologicalSpace X›` depends on `i : MeasurableSpace X`, but this message isn't readable:
```lean
failed to create binder due to failure when reverting variable dependencies
```
This is probrem in this case:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/borelize.20gives.20.22failed.20to.20create.20binder.2E.2E.2E.22

This PR make  error messages more readable:
```lean
‹TopologicalSpace X› := (expr depends on i)"
depends on
i : MeasurableSpace X
so `borelize` isn't avaliable
```

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -231,13 +231,21 @@ def addBorelInstance (e : Expr) : 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
+  let te ← Lean.Elab.Term.exprToSyntax e
   evalTactic <| ← `(tactic|
-    have := @BorelSpace.measurable_eq $t _ _ _)
-  liftMetaTactic fun m => return [← subst m i]
+    have := @BorelSpace.measurable_eq $te _ _ _)
+  try
+    liftMetaTactic fun m => return [← subst m i]
+  catch _ =>
+    let et ← synthInstance (← mkAppOptM ``TopologicalSpace #[e])
+    throwError
+      (m!"`‹TopologicalSpace {e}› := {et}" ++ MessageData.ofFormat Format.line ++
+        m!"depends on" ++ MessageData.ofFormat Format.line ++
+        m!"{Expr.fvar i} : MeasurableSpace {e}`" ++ MessageData.ofFormat Format.line ++
+        "so `borelize` isn't avaliable")
   evalTactic <| ← `(tactic|
     refine_lift
-      letI : MeasurableSpace $t := borel $t
+      letI : MeasurableSpace $te := borel $te
       ?_)
 
 /-- Given a type `$t`, if there is an assumption `[i : MeasurableSpace $t]`, then try to prove