awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
pos : ∀ (ha : ∀ b < a, (Ioo b a).Nonempty), MeasurableSet (Iio a)
⊢ MeasurableSet (Iio a)
have neg : ∀ (ha : ∃ b < a, Ioo b a = ∅), MeasurableSet (Iio a)
Tactic: by_cases! ha : ∀ b < a, (Ioo b a).Nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (Iio a)
have h : Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
h : Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u
⊢ MeasurableSet (Iio a)
have pos : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u
have h : ∀ (y : α), y ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
⊢ y ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u) y
have h : y < a ↔ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
Tactic: push _ ∈ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
⊢ y < a ↔ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
have h : y < a → ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
h : y < a → ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
⊢ y < a ↔ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
have h₁ : (∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1) → y < a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
hy : y < a
⊢ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
have h : ∀ (l : α) (hlt : l ∈ t) (hly : l ≤ y),
  ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
Tactic: rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
hy : y < a
l : α
hlt : l ∈ t
hly : l ≤ y
⊢ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
have h : ∀ (u : α) (hut : u ∈ t) (hyu : y < u) (hua : u < a),
  ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
Tactic: rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)
have pos : ∀ (a_1 : α) (ha : a_1 ∈ t) (b : α) (hb : b ∈ t),
  MeasurableSet.{u_5} (α := α) (⋃ (_ : a_1 < b), ⋃ (_ : b < a), Icc a_1 b)
Tactic: refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a_1 : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha_1 : ∀ b < a_1, (Ioo b a_1).Nonempty
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ MeasurableSet.{u_5} (α := α) (⋃ (_ : a < b), ⋃ (_ : b < a_1), Icc a b)
have pos : ∀ (hab : a < b), b < a_1 → MeasurableSet (Icc a b)
Tactic: refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∃ b < a, Ioo b a = ∅
⊢ MeasurableSet (Iio a)
have neg : ∀ (b : α) (ba : b < a) (hb : Ioo b a = ∅), MeasurableSet (Iio a)
Tactic: rcases ha with ⟨b, ba, hb⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
⊢ MeasurableSet (Iio a)
have hbs : b ∈ s
Tactic: have hbs : b ∈ s := hIoo b a ba hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ MeasurableSet (Iio a)
have h : Iio a = ⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
h : Iio a = ⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b
⊢ MeasurableSet (Iio a)
have neg : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b)
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ Iio a = ⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b
have h : ∀ (x : α), x ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
⊢ x ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b) x
have h : x < a ↔ ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
Tactic: simp only [mem_Iio, mem_iUnion, mem_Icc, exists_and_left, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
y : α
yx : y ≤ x
hy1 : y ≤ b
hy2 : y ∈ t
hy : x ≤ b
⊢ x < a
have order : ¬x < a → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
y : α
yx : y ≤ x
hy1 : y ≤ b
hy2 : y ∈ t
hy : x ≤ b
order order₁ order₂ order₃ : ¬x < a → False
⊢ x < a
have order₄ : a ≤ x → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
⊢ x < a ↔ ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
have h : ∀ (h : x < a), ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
Tactic: refine ⟨fun h ↦ ?_, fun ⟨y, yx, hy1, hy2, hy⟩ ↦ by order⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
⊢ x ≤ b
have contrapose! : ∀ (hb : b < x), (Ioo b a).Nonempty
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
⊢ ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
have this₁ : x ≤ b
Tactic: have : x ≤ b := by
        contrapose! hb
        exact ⟨x, hb, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
⊢ ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
have h₁ : ∀ (z : α) (hzt : z ∈ t) (hzx : z ≤ x), ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
Tactic: rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ z ≤ b
have order : ¬z ≤ b → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
order order₁ order₂ order₃ : ¬z ≤ b → False
⊢ z ≤ b
have order₄ : b < z → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ x ≤ b
have order : ¬x ≤ b → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
order order₁ order₂ order₃ : ¬x ≤ b → False
⊢ x ≤ b
have order₄ : b < x → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b)
have neg : ∀ (x : α) (hx : x ∈ t) (hlt : x ≤ b), MeasurableSet (Icc x b)
Tactic: refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α
have h : ∀ (t_1 : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} t_1 → MeasurableSet t_1
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
⊢ ∀ (t_1 : Set α),
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} t_1 → MeasurableSet t_1
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
⊢ borel α = MeasurableSpace.generateFrom S
have refine : borel α ≤ MeasurableSpace.generateFrom S
Tactic: refine le_antisymm ?_ (generateFrom_Ico_mem_le_borel _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
⊢ borel α ≤ MeasurableSpace.generateFrom S
have rw : MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
Tactic: rw [borel_eq_generateFrom_Iio]