-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem borel_eq_generateFrom_Iic :
    borel α = MeasurableSpace.generateFrom (range Iic)

Proof state:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => ?_

Result:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Ioi
⊢ MeasurableSet t

Proof state:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => ?_

Result:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Iic
⊢ MeasurableSet t

Proof state:
case refine_1.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)

Tactic:
rw [← compl_Iic]

Result:
case refine_1.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)ᶜ

Proof state:
case refine_1.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Iic
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Result:
case refine_2.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)

Proof state:
case refine_2.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Ioi
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Result:
case refine_1.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)

Proof state:
case refine_2.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)

Tactic:
rw [← compl_Ioi]

Result:
case refine_2.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)

case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iic)

Tactic:
rw [borel_eq_generateFrom_Ioi]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)