awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
pos : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)
⊢ MeasurableSet (Iio a)

Tactic:
convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u ≤ a), Ico l u)

Premises used: MeasurableSet, Set.Ico, Set.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u) y

Tactic:
push _ ∈ _
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
h₁ : (∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1) → y < a
⊢ y < a ↔ ∃ (i : α) (_ : i ∈ t) (i_1 : α) (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ ∃ (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⟩

Premises used: Dense.exists_le'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ ∃ (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⟩

Premises used: isOpen_Ioo, Dense.exists_mem_open
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩

Premises used: LT.lt.le, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 l u : α
hua : u ≤ a
hyu : y < u
⊢ y < a

Tactic:
hyu.trans_le hua

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 l u : α
hua : u ≤ a
hyu : y < u
⊢ y < a

Tactic:
exact hyu.trans_le hua

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)

Tactic:
MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
pos :
  ∀ (a_1 : α) (ha : a_1 ∈ t) (b : α) (hb : b ∈ t),
    MeasurableSet.{u_5} (α := α) (⋃ (_ : a_1 < b), ⋃ (_ : b ≤ a), Ico a_1 b)
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)

Tactic:
refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)

Tactic:
MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
pos : ∀ (hab : a < b), b ≤ a_1 → MeasurableSet (Ico a b)
⊢ MeasurableSet.{u_5} (α := α) (⋃ (_ : a < b), ⋃ (_ : b ≤ a_1), Ico a b)

Tactic:
refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
hab : a < b
h : b ≤ a_1
⊢ MeasurableSet (Ico a b)

Tactic:
.basic _ ⟨a, hts ha, b, hts hb, hab, mem_singleton _⟩

Premises used: Set.mem_singleton, MeasurableSet, MeasurableSpace.GenerateMeasurable.basic, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
hab : a < b
h : b ≤ a_1
⊢ MeasurableSet (Ico a b)

Tactic:
exact .basic _ ⟨a, hts ha, b, hts hb, hab, mem_singleton _⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 = ∅
⊢ a ∈ s

Tactic:
replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.1 ha.choose_spec.2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
neg : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l < a), Ico l a)
⊢ MeasurableSet (Iio a)

Tactic:
convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)

Premises used: MeasurableSet, Set.Ico, Set.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a = Iio a
⊢ Iio a = ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ∀ x < a, ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x
⊢ ⋃ l ∈ t, ⋃ (_ : l < a), Ico l a = Iio a

Tactic:
simp only [← Ici_inter_Iio, ← iUnion_inter, inter_eq_right, subset_def, mem_iUnion,
        mem_Ici, mem_Iio]

Premises used: Set.mem_Iio, Set.Ici_inter_Iio, Set.subset_def, Set.mem_iUnion, Set.inter_eq_right, Set.iUnion_inter, Set.mem_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
h : ∀ (z : α) (hzt : z ∈ t) (hzx : z ≤ x), ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ 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⟩

Premises used: Dense.exists_le'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x

Tactic:
⟨z, hzt, hzx.trans_lt hx, hzx⟩

Premises used: Exists.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ ∃ (i : α) (_ : i ∈ t) (_ : i < a), i ≤ x

Tactic:
exact ⟨z, hzt, hzx.trans_lt hx, hzx⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)

Tactic:
.biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_

Premises used: MeasurableSet.biUnion, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
neg : ∀ (x : α) (hx : x ∈ t) (hlt : x < a), MeasurableSet (Ico x a)
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ (_ : l < a), Ico l a)

Tactic:
refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∈ t
hlt : x < a
⊢ MeasurableSet (Ico x a)

Tactic:
.basic _ ⟨x, hts hx, a, ha, hlt, mem_singleton _⟩

Premises used: Set.mem_singleton, MeasurableSet, MeasurableSpace.GenerateMeasurable.basic, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∈ t
hlt : x < a
⊢ MeasurableSet (Ico x a)

Tactic:
exact .basic _ ⟨x, hts hx, a, ha, hlt, mem_singleton _⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Ico l u = S}

Tactic:
simpa only [exists_prop, mem_univ, true_and] using
    (@dense_univ α _).borel_eq_generateFrom_Ico_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _

Premises used: dense_univ, exists_prop, Dense.borel_eq_generateFrom_Ico_mem_aux, Set.mem_univ, true_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
⊢ Eq.{u_5 + 1} (α := MeasurableSpace αᵒᵈ) (borel αᵒᵈ)
    (MeasurableSpace.generateFrom
      {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:
hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _

Premises used: Dense.borel_eq_generateFrom_Ico_mem_aux, Dense.orderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
hbot₁ : ∀ (x y : αᵒᵈ) (hlt : x < y) (he : Ioo x y = ∅), Ioo y x = ∅
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc 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

Premises used: Dense.borel_eq_generateFrom_Ico_mem_aux, Dense.orderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : α = αᵒᵈ
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
⊢ 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:
ext s