α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
⊢ borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
let g : MeasurableSpace ℝ := .generateFrom (⋃ a : ℚ, {Iio (a : ℝ)})
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ borel ℝ ≤ MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})

case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a}) ≤ borel ℝ
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
refine' le_antisymm _ _
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ MeasurableSpace.generateFrom (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) ≤
    MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ borel ℝ ≤ MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
rw [borel_eq_generateFrom_Ioo_rat]
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t✝ u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
t : Set ℝ
⊢ (t ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → MeasurableSet t
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ MeasurableSpace.generateFrom (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) ≤
    MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
refine' generateFrom_le fun t => _
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t✝ u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
t : Set ℝ
⊢ (∃ i i_1 h, t = Ioo ↑i ↑i_1) → MeasurableSet t
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t✝ u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
t : Set ℝ
⊢ (t ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → MeasurableSet t
simp only [mem_iUnion, mem_singleton_iff]
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
⊢ MeasurableSet (Ioo ↑a ↑b)
case refine'_1
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t✝ u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
t : Set ℝ
⊢ (∃ i i_1 h, t = Ioo ↑i ↑i_1) → MeasurableSet t
rintro ⟨a, b, _, rfl⟩
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
⊢ MeasurableSet ((⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
⊢ MeasurableSet (Ioo ↑a ↑b)
rw [(Set.ext fun x => by
      suffices x < ↑b → (↑a < x ↔ ∃ i : ℚ, a < i ∧ ↑i ≤ x) by simpa
      refine' fun _ => ⟨fun h => _, fun ⟨i, hai, hix⟩ => (Rat.cast_lt.2 hai).trans_le hix⟩
      rcases exists_rat_btwn h with ⟨c, ac, cx⟩
      exact ⟨c, Rat.cast_lt.1 ac, cx.le⟩
        : Ioo (a : ℝ) b = (⋃ c > a, Iio (c : ℝ)ᶜ) ∩ Iio (b : ℝ))]
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
⊢ x < ↑b → (↑a < x ↔ ∃ i, a < i ∧ ↑i ≤ x)
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
⊢ x ∈ Ioo ↑a ↑b ↔ x ∈ (⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b
suffices x < ↑b → (↑a < x ↔ ∃ i : ℚ, a < i ∧ ↑i ≤ x) by simpa
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
x✝ : x < ↑b
h : ↑a < x
⊢ ∃ i, a < i ∧ ↑i ≤ x
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
⊢ x < ↑b → (↑a < x ↔ ∃ i, a < i ∧ ↑i ≤ x)
refine' fun _ => ⟨fun h => _, fun ⟨i, hai, hix⟩ => (Rat.cast_lt.2 hai).trans_le hix⟩
case intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
x✝ : x < ↑b
h : ↑a < x
c : ℚ
ac : ↑a < ↑c
cx : ↑c < x
⊢ ∃ i, a < i ∧ ↑i ≤ x
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
x✝ : x < ↑b
h : ↑a < x
⊢ ∃ i, a < i ∧ ↑i ≤ x
rcases exists_rat_btwn h with ⟨c, ac, cx⟩
no goals
case intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
x✝ : x < ↑b
h : ↑a < x
c : ℚ
ac : ↑a < ↑c
cx : ↑c < x
⊢ ∃ i, a < i ∧ ↑i ≤ x
exact ⟨c, Rat.cast_lt.1 ac, cx.le⟩
no goals
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
x : ℝ
this : x < ↑b → (↑a < x ↔ ∃ i, a < i ∧ ↑i ≤ x)
⊢ x ∈ Ioo ↑a ↑b ↔ x ∈ (⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b
simpa
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
⊢ MeasurableSet ((⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
⊢ MeasurableSet ((⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b)
have hg : ∀ q : ℚ, MeasurableSet[g] (Iio (q : ℝ)) := fun q =>
  GenerateMeasurable.basic (Iio (q : ℝ)) (by simp)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
⊢ MeasurableSet (⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
⊢ MeasurableSet ((⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ) ∩ Iio ↑b)
refine' @MeasurableSet.inter _ g _ _ _ (hg _)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
c : ℚ
x✝ : c ∈ fun c => Rat.blt a c = true
⊢ MeasurableSet (Iio ↑cᶜ)
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
⊢ MeasurableSet (⋃ (c : ℚ) (_ : c > a), Iio ↑cᶜ)
refine' @MeasurableSet.biUnion _ _ g _ _ (to_countable _) fun c _ => _
no goals
case refine'_1.intro.intro.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
hg : ∀ (q : ℚ), MeasurableSet (Iio ↑q)
c : ℚ
x✝ : c ∈ fun c => Rat.blt a c = true
⊢ MeasurableSet (Iio ↑cᶜ)
exact @MeasurableSet.compl _ _ g (hg _)
no goals
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
a b : ℚ
w✝ : a < b
q : ℚ
⊢ Iio ↑q ∈ ⋃ (a : ℚ), {Iio ↑a}
simp
case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
x✝ : Set ℝ
⊢ (x✝ ∈ ⋃ (a : ℚ), {Iio ↑a}) → MeasurableSet x✝
case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
⊢ MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a}) ≤ borel ℝ
refine' MeasurableSpace.generateFrom_le fun _ => _
case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
x✝ : Set ℝ
⊢ (∃ i, x✝ = Iio ↑i) → MeasurableSet x✝
case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
x✝ : Set ℝ
⊢ (x✝ ∈ ⋃ (a : ℚ), {Iio ↑a}) → MeasurableSet x✝
simp only [mem_iUnion, mem_singleton_iff]
case refine'_2.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
r : ℚ
⊢ MeasurableSet (Iio ↑r)
case refine'_2
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
x✝ : Set ℝ
⊢ (∃ i, x✝ = Iio ↑i) → MeasurableSet x✝
rintro ⟨r, rfl⟩
no goals
case refine'_2.intro
α : Type ?u.2518610
β : Type ?u.2518613
γ : Type ?u.2518616
γ₂ : Type ?u.2518619
δ : Type ?u.2518622
ι : Sort y
s t u : Set α
g : MeasurableSpace ℝ := MeasurableSpace.generateFrom (⋃ (a : ℚ), {Iio ↑a})
r : ℚ
⊢ MeasurableSet (Iio ↑r)
exact @measurableSet_Iio _ _ (borel ℝ) _ _ _ _