-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s)
    (hbot : ∀ x, IsTop x → x ∈ s) (hIoo : ∀ x y : α, x < y → Ioo x y = ∅ → x ∈ s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S }

Proof state:
case h.e'_3.h.h.e'_2.h.h.mp.intro.intro.intro.intro.intro
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Ioc l u ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

case h.e'_3.h.h.e'_2.h.h.mpr.intro.intro.intro.intro.intro
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : αᵒᵈ
hl : l ∈ ⇑OrderDual.ofDual ⁻¹' s
u : αᵒᵈ
hu : u ∈ ⇑OrderDual.ofDual ⁻¹' s
hlt : l < u
⊢ Ico l u ∈ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}

Tactic:
exacts [⟨u, hu, l, hl, hlt, dual_Ico⟩, ⟨u, hu, l, hl, hlt, dual_Ioc⟩]

Result:
no goals

Proof state:
case h.e'_3.h.h.e'_2.h
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} =
    {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

Tactic:
ext s

Result:
case h.e'_3.h.h.e'_2.h.h
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} ↔
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

Proof state:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ ⇑OrderDual.ofDual ⁻¹' Ioo x y = ∅

Tactic:
exact he

Result:
no goals

Proof state:
case h.e'_3.h.h.e'_2.h.h
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} ↔
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

Tactic:
constructor <;> rintro ⟨l, hl, u, hu, hlt, rfl⟩

Result:
case h.e'_3.h.h.e'_2.h.h.mp.intro.intro.intro.intro.intro
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Ioc l u ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

case h.e'_3.h.h.e'_2.h.h.mpr.intro.intro.intro.intro.intro
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : αᵒᵈ
hl : l ∈ ⇑OrderDual.ofDual ⁻¹' s
u : αᵒᵈ
hu : u ∈ ⇑OrderDual.ofDual ⁻¹' s
hlt : l < u
⊢ Ico l u ∈ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}

Proof state:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅

Tactic:
erw [dual_Ioo]

Result:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ ⇑OrderDual.ofDual ⁻¹' Ioo x y = ∅

Proof state:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}

Tactic:
convert hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _
  using 2

Result:
case h.e'_3.h.h.e'_2.h
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} =
    {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅