α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iic)
rw [borel_eq_generateFrom_Ioi]
case refine'_1
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)

case refine'_2
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)
refine' le_antisymm _ _
case refine'_1
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t✝ u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Ioi
⊢ MeasurableSet t
case refine'_1
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)
refine' MeasurableSpace.generateFrom_le fun t ht => _
case refine'_1.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)
case refine'_1
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t✝ u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Ioi
⊢ MeasurableSet t
obtain ⟨u, rfl⟩ := ht
case refine'_1.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic uᶜ)
case refine'_1.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)
rw [← compl_Iic]
no goals
case refine'_1.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic uᶜ)
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl
case refine'_2
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t✝ u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Iic
⊢ MeasurableSet t
case refine'_2
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)
refine' MeasurableSpace.generateFrom_le fun t ht => _
case refine'_2.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)
case refine'_2
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t✝ u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Iic
⊢ MeasurableSet t
obtain ⟨u, rfl⟩ := ht
case refine'_2.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi uᶜ)
case refine'_2.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)
rw [← compl_Ioi]
no goals
case refine'_2.intro
α : Type u_1
β : Type ?u.119737
γ : Type ?u.119740
γ₂ : Type ?u.119743
δ : Type ?u.119746
ι : Sort y
s t u✝ : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi uᶜ)
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl