case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)

case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (t : Set α), t ∈ range Iio → MeasurableSet t
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)
refine' le_antisymm _ (generateFrom_le _)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)
rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
letI : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ ∀ (t : Set α), t ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a} → MeasurableSet t
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
refine' generateFrom_le _
case refine'_1.intro.inl
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Ioi a)
case refine'_1
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ ∀ (t : Set α), t ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a} → MeasurableSet t
rintro _ ⟨a, rfl | rfl⟩ <;> [skip; apply H]
case pos
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ∃ a', ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)

case neg
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)
case refine'_1.intro.inl
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Ioi a)
by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b
case pos.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)
case pos
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ∃ a', ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)
rcases h with ⟨a', ha'⟩
case pos.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Iio a'ᶜ)

α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ Ioi a = Iio a'ᶜ
case pos.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)
rw [(_ : Ioi a = Iio a'ᶜ)]
no goals
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ Ioi a = Iio a'ᶜ
simp [Set.ext_iff, ha']
no goals
case pos.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a a' : α
ha' : ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Iio a'ᶜ)
exact (H _).compl
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
vu : (⋃ (i : { a' // a < a' }) (_ : i ∈ v), {b | ↑i < b}) = ⋃ (i : { a' // a < a' }), {b | ↑i < b}
hv : Encodable ↑v
⊢ MeasurableSet (Ioi a)
case neg
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
⊢ MeasurableSet (Ioi a)
rcases isOpen_iUnion_countable (fun a' : { a' : α // a < a' } => { b | a'.1 < b }) fun a' =>
    isOpen_lt' _ with ⟨v, ⟨hv⟩, vu⟩
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
⊢ MeasurableSet (Ioi a)
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
vu : (⋃ (i : { a' // a < a' }) (_ : i ∈ v), {b | ↑i < b}) = ⋃ (i : { a' // a < a' }), {b | ↑i < b}
hv : Encodable ↑v
⊢ MeasurableSet (Ioi a)
simp [Set.ext_iff] at vu
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ MeasurableSet (⋃ (x : ↑v), Iio ↑↑xᶜ)
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ MeasurableSet (Ioi a)
rw [this]
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ MeasurableSet (⋃ (x : ↑v), Iio ↑↑xᶜ)
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ MeasurableSet (⋃ (x : ↑v), Iio ↑↑xᶜ)
skip
case neg.intro.intro.intro.h
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ ∀ (b : ↑v), MeasurableSet (Iio ↑↑bᶜ)
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ MeasurableSet (⋃ (x : ↑v), Iio ↑↑xᶜ)
apply MeasurableSet.iUnion
no goals
case neg.intro.intro.intro.h
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
this : Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
⊢ ∀ (b : ↑v), MeasurableSet (Iio ↑↑bᶜ)
exact fun _ => (H _).compl
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
⊢ ∀ (x : α), a < x ↔ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
⊢ Ioi a = ⋃ (x : ↑v), Iio ↑↑xᶜ
simp [Set.ext_iff]
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
⊢ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
⊢ ∀ (x : α), a < x ↔ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
refine' fun x => ⟨fun ax => _, fun ⟨a', ⟨h, _⟩, ax⟩ => lt_of_lt_of_le h ax⟩
case intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
a' : α
h₁ : ∃ x, { val := a', property := (_ : a < a') } ∈ v
h₂ : a' < x
⊢ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
⊢ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
rcases (vu x).2 (by
  refine' not_imp_comm.1 (fun h => _) h
  exact ⟨x, fun b =>
    ⟨fun ab => le_of_not_lt fun h' => h ⟨b, ab, h'⟩, lt_of_lt_of_le ax⟩⟩) with ⟨a', h₁, h₂⟩
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h✝ : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
h : ¬∃ a_1, a < a_1 ∧ a_1 < x
⊢ ∃ a', ∀ (b : α), a < b ↔ a' ≤ b
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
⊢ ∃ a_1, a < a_1 ∧ a_1 < x
refine' not_imp_comm.1 (fun h => _) h
no goals
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h✝ : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
h : ¬∃ a_1, a < a_1 ∧ a_1 < x
⊢ ∃ a', ∀ (b : α), a < b ↔ a' ≤ b
exact ⟨x, fun b =>
  ⟨fun ab => le_of_not_lt fun h' => h ⟨b, ab, h'⟩, lt_of_lt_of_le ax⟩⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
h : ¬∃ a', ∀ (b : α), a < b ↔ a' ≤ b
v : Set { a' // a < a' }
hv : Encodable ↑v
vu : ∀ (x : α), (∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 < x) ↔ ∃ a_1, a < a_1 ∧ a_1 < x
x : α
ax : a < x
a' : α
h₁ : ∃ x, { val := a', property := (_ : a < a') } ∈ v
h₂ : a' < x
⊢ ∃ a_1, (∃ x, { val := a_1, property := (_ : a < a_1) } ∈ v) ∧ a_1 ≤ x
exact ⟨a', h₁, le_of_lt h₂⟩
case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (i : α), MeasurableSet (Iio i)
case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (t : Set α), t ∈ range Iio → MeasurableSet t
rw [forall_range_iff]
case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ MeasurableSet (Iio a)
case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (i : α), MeasurableSet (Iio i)
intro a
no goals
case refine'_2
α : Type u_1
β : Type ?u.82061
γ : Type ?u.82064
γ₂ : Type ?u.82067
δ : Type ?u.82070
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ MeasurableSet (Iio a)
exact GenerateMeasurable.basic _ isOpen_Iio