bug in `borelize`

Stream: mathlib4

[Yury G. Kudryashov]

The following examples fail:

import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

example : True := by
  obtain ⟨α, ⟨hα⟩⟩ : ∃ α : Type, Nonempty (TopologicalSpace α) := ⟨ℕ, ⟨inferInstance⟩⟩
  borelize α

example : True := by
  set α := ℕ
  borelize α

[Yury G. Kudryashov]

The set version appears in !4#4929

[Kyle Miller]

It looks like it's because of a missing withMainContext. I'll create a PR

[Kyle Miller]

mathlib4#5237

[Kyle Miller]

If anyone wants to take a look at a little bit of meta code, mathlib4#5237 has passed CI and it adds tests.