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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
⊢ MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
have refine : ∀ (a : α), MeasurableSet (Iio a)
Tactic: refine generateFrom_le (forall_mem_range.2 fun a => ?_)
-- 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
a : α
⊢ MeasurableSet (Iio a)
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (hc : t.Countable) (htd : Dense t) (htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t),
  MeasurableSet (Iio a)
Tactic: rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
⊢ MeasurableSet (Iio a)
have pos : ∀ (ha : ∀ b < a, (Ioo b a).Nonempty), 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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), Ico l u
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u ≤ a), Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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), Ico l u
⊢ MeasurableSet (Iio a)
have pos : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u ≤ a), Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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), Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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), Ico l u)
have pos : ∀ (a_1 : α) (ha : a_1 ∈ t) (b : α) (hb : b ∈ t),
  MeasurableSet.{u_5} (α := α) (⋃ (_ : a_1 < b), ⋃ (_ : b ≤ a), Ico 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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), Ico a b)
have pos : ∀ (hab : a < b), b ≤ a_1 → MeasurableSet (Ico a b)
Tactic: refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
-- 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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 ha₁ : a ∈ s
Tactic: replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.1 ha.choose_spec.2
Cleared hypotheses: ha
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
⊢ MeasurableSet (Iio a)
have h : Iio a = ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
h : Iio a = ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a
⊢ MeasurableSet (Iio a)
have neg : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l < a), Ico l a)
Tactic: convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
⊢ Iio a = ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a
have h : ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a = Iio a
Tactic: symm
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
⊢ ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a = Iio a
have h : ∀ x < a, ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x
Tactic: simp only [← Ici_inter_Iio, ← iUnion_inter, inter_eq_right, subset_def, mem_iUnion,
        mem_Ici, mem_Iio]
-- 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
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
x : α
hx : x < a
⊢ ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x
have h : ∀ (z : α) (hzt : z ∈ t) (hzx : z ≤ x), ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x
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 = ∅ → y ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico 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 : a ∈ s
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l < a), Ico l a)
have neg : ∀ (x : α) (hx : x ∈ t) (hlt : x < a), MeasurableSet (Ico x a)
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 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
have h : MeasurableSpace α = MeasurableSpace αᵒᵈ →
  α = αᵒᵈ →
    Eq.{u_5 + 1} (α := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
Tactic: convert!
    hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _ using 2
-- 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 : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
h :
  MeasurableSpace α = MeasurableSpace αᵒᵈ →
    α = αᵒᵈ →
      Eq.{u_5 + 1} (α := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
        {S : Set αᵒᵈ |
          ∃ (l : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
              ∃ (u : αᵒᵈ),
                Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
have hbot₁ : ∀ (x y : αᵒᵈ) (hlt : x < y) (he : Ioo x y = ∅), Ioo y x = ∅
Tactic: convert!
    hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _ using 2
-- 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 : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
⊢ Eq.{u_5 + 1} (α := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
    {S : Set αᵒᵈ |
      ∃ (l : αᵒᵈ),
        Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
          ∃ (u : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
have h : ∀ (s_1 : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} s_1 ↔
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s) u ∧ l < u ∧ Ico l u = S}
      s_1
Tactic: ext s
-- 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_1 : Set α
hd : Dense s_1
hbot : ∀ (x : α), IsTop x → x ∈ s_1
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s_1
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s ↔
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s
have h : Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s →
  Membership.mem (γ := Set (Set α))
    {S : Set αᵒᵈ |
      ∃ (l : αᵒᵈ),
        Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
          ∃ (u : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
    s
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_1 : Set α
hd : Dense s_1
hbot : ∀ (x : α), IsTop x → x ∈ s_1
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s_1
e_1 : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1_1 : α = αᵒᵈ
s : Set α
h :
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s →
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s
⊢ Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s ↔
    Membership.mem (γ := Set (Set α))
      {S : Set αᵒᵈ |
        ∃ (l : αᵒᵈ),
          Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
            ∃ (u : αᵒᵈ),
              Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
      s
have h₁ : Membership.mem (γ := Set (Set α))
    {S : Set αᵒᵈ |
      ∃ (l : αᵒᵈ),
        Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) l ∧
          ∃ (u : αᵒᵈ),
            Membership.mem (γ := Set αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s_1) u ∧ l < u ∧ Ico l u = S}
    s →
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s_1, ∃ u ∈ s_1, l < u ∧ Ioc l u = S} s
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 : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅
have erw : Eq (α := Set α) ((⇑OrderDual.ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ) ⁻¹' Ioo x y) ∅
Tactic: erw [Ioo_toDual]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
have a : borel α ≤ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : borel α ≤ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
have a₁ : MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} ≤ borel α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
have a : LE.le.{u_5} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ioc l u = S})
  (MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S})
Tactic: rw [borel_eq_generateFrom_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} ≤ borel α
have a : ∀ (t : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S} t → MeasurableSet t
Tactic: apply generateFrom_le