-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem MeasurableSet.residualEq_isOpen [MeasurableSpace α] [BorelSpace α] (h : MeasurableSet s) :
    ∃ u : Set α, IsOpen u ∧ s =ᵇ u

Proof state:
case right
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
U : Set α
Uo : IsOpen U
hsU : s =ᶠ[residual α] U
⊢ sᶜ =ᶠ[residual α] (closure U)ᶜ

Tactic:
exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed

Result:
no goals

Proof state:
case isOpen
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
U : Set α
hU : IsOpen U
⊢ ∃ u, IsOpen u ∧ U =ᶠ[residual α] u

Tactic:
exact ⟨U, hU, .rfl⟩

Result:
no goals

Proof state:
case iUnion
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : ℕ → Set α
a✝ : Pairwise (Function.onFun Disjoint f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∃ u, IsOpen u ∧ f i =ᶠ[residual α] u
⊢ ∃ u, IsOpen u ∧ ⋃ i, f i =ᶠ[residual α] u

Tactic:
choose u uo su using ihf

Result:
case iUnion
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : ℕ → Set α
a✝ : Pairwise (Function.onFun Disjoint f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
u : ℕ → Set α
uo : ∀ (i : ℕ), IsOpen (u i)
su : ∀ (i : ℕ), f i =ᶠ[residual α] u i
⊢ ∃ u, IsOpen u ∧ ⋃ i, f i =ᶠ[residual α] u

Proof state:
case compl
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
ihs : ∃ u, IsOpen u ∧ s =ᶠ[residual α] u
⊢ ∃ u, IsOpen u ∧ sᶜ =ᶠ[residual α] u

Tactic:
obtain ⟨U, Uo, hsU⟩ := ihs

Result:
case compl.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
U : Set α
Uo : IsOpen U
hsU : s =ᶠ[residual α] U
⊢ ∃ u, IsOpen u ∧ sᶜ =ᶠ[residual α] u

Proof state:
case compl.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
U : Set α
Uo : IsOpen U
hsU : s =ᶠ[residual α] U
⊢ ∃ u, IsOpen u ∧ sᶜ =ᶠ[residual α] u

Tactic:
use (closure U)ᶜ, isClosed_closure.isOpen_compl

Result:
case right
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
U : Set α
Uo : IsOpen U
hsU : s =ᶠ[residual α] U
⊢ sᶜ =ᶠ[residual α] (closure U)ᶜ

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
h : MeasurableSet s
⊢ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u

Tactic:
induction s, h using MeasurableSet.induction_on_open with
| isOpen U hU => exact ⟨U, hU, .rfl⟩
| compl s _ ihs =>
  obtain ⟨U, Uo, hsU⟩ := ihs
  use (closure U)ᶜ, isClosed_closure.isOpen_compl
  exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed
| iUnion f _ _ ihf =>
  choose u uo su using ihf
  exact ⟨⋃ i, u i, isOpen_iUnion uo, EventuallyEq.countable_iUnion su⟩

Result:
no goals

Proof state:
case iUnion
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : ℕ → Set α
a✝ : Pairwise (Function.onFun Disjoint f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
u : ℕ → Set α
uo : ∀ (i : ℕ), IsOpen (u i)
su : ∀ (i : ℕ), f i =ᶠ[residual α] u i
⊢ ∃ u, IsOpen u ∧ ⋃ i, f i =ᶠ[residual α] u

Tactic:
exact ⟨⋃ i, u i, isOpen_iUnion uo, EventuallyEq.countable_iUnion su⟩

Result:
no goals