awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
a b x : α
μ : Measure α
inst_3 : OrderClosedTopology α
⊢ (𝓝[[[a, b]]] x).IsMeasurablyGenerated

Tactic:
nhdsWithin_Icc_isMeasurablyGenerated

Premises used: Set.uIcc, nhdsWithin_Icc_isMeasurablyGenerated
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
⊢ MeasurableSet.{u_1} (α := α × α) {p : α × α | p.1 < p.2}

Tactic:
(isOpen_lt continuous_fst continuous_snd).measurableSet

Premises used: isOpen_lt, continuous_snd, continuous_fst, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
⊢ Measurable (β := Prop) fun (p : α × α) ↦ p.1 < p.2

Tactic:
measurableSet_setOf.mp measurableSet_lt'

Premises used: measurableSet_setOf, Iff.mp, measurableSet_lt'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet.{u_4} (α := δ) {a : δ | f a < g a}

Tactic:
hf.prodMk hg measurableSet_lt'

Premises used: Set.Mem, setOf, Measurable.prodMk, Set.preimage, measurableSet_lt'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := Prop) fun (a : δ) ↦ f a < g a

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
μ : Measure δ
f g : δ → α
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ NullMeasurableSet {a : δ | f a < g a} μ

Tactic:
(hf.prodMk hg).nullMeasurable measurableSet_lt'

Premises used: AEMeasurable.nullMeasurable, Set.Mem, setOf, Set.preimage, AEMeasurable.prodMk, measurableSet_lt'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
μ : Measure (α × α)
⊢ NullMeasurableSet {p : α × α | p.1 < p.2} μ

Tactic:
measurableSet_lt'.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_lt'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : SecondCountableTopology α
inst_4 : OrderClosedTopology α
μ : Measure δ
f g : δ → α
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ NullMeasurableSet {a : δ | f a ≤ g a} μ

Tactic:
(hf.prodMk hg).nullMeasurable measurableSet_le'

Premises used: AEMeasurable.nullMeasurable, Set.Mem, setOf, Set.preimage, AEMeasurable.prodMk, measurableSet_le'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ IsOpen[inst] u

Tactic:
have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
⊢ MeasurableSet u

Tactic:
have humeas : MeasurableSet u := huopen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
⊢ (s \ u).Finite

Tactic:
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
⊢ u ⊆ s

Tactic:
have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy =>
    Ioo_subset_Icc_self.trans (h.out hx hy)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
rw : MeasurableSet (u ∪ s \ u)
⊢ MeasurableSet s

Tactic:
rw [← union_diff_cancel this]

Premises used: Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet (u ∪ s \ u)

Tactic:
humeas.union hfinite.measurableSet

Premises used: MeasurableSet.union, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet (u ∪ s \ u)

Tactic:
exact humeas.union hfinite.measurableSet

Premises used: MeasurableSet.union, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : IsPreconnected s
⊢ MeasurableSet s

Tactic:
h.ordConnected.measurableSet

Premises used: Set.OrdConnected.measurableSet, IsPreconnected.ordConnected
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
h :
  ∀ (t_1 : Set α),
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} t_1 → MeasurableSet t_1
⊢ MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} ≤ borel α

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
a b : α
⊢ MeasurableSet (Icc a b)

Tactic:
measurableSet_Icc

Premises used: measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
a b : α
⊢ MeasurableSet (Icc a b)

Tactic:
exact measurableSet_Icc

Premises used: measurableSet_Icc
-- 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 = ∅ → x ∈ s
set :
  let S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S};
  borel α = MeasurableSpace.generateFrom S
⊢ borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}

Tactic:
set S : Set (Set α) := { S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S }

Premises used: Set
-- 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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
⊢ borel α = MeasurableSpace.generateFrom S

Tactic:
le_antisymm ?_ (generateFrom_Icc_mem_le_borel _ _)

Premises used: generateFrom_Icc_mem_le_borel, le_antisymm
-- 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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
refine : borel α ≤ MeasurableSpace.generateFrom S
⊢ borel α = MeasurableSpace.generateFrom S

Tactic:
refine le_antisymm ?_ (generateFrom_Icc_mem_le_borel _ _)

Premises used: generateFrom_Icc_mem_le_borel, le_antisymm
-- 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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
rw : MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
⊢ borel α ≤ MeasurableSpace.generateFrom S

Tactic:
rw [borel_eq_generateFrom_Iio]

Premises used: borel_eq_generateFrom_Iio
-- 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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
⊢ MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S

Tactic:
generateFrom_le (forall_mem_range.2 fun a => ?_)

Premises used: Iff.mpr, Set.forall_mem_range, MeasurableSpace.generateFrom_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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
refine : ∀ (a : α), MeasurableSet (Iio a)
⊢ MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S

Tactic:
refine generateFrom_le (forall_mem_range.2 fun a => ?_)

Premises used: Iff.mpr, Set.forall_mem_range, MeasurableSpace.generateFrom_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 = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
rcases :
  ∀ (t : Set α) (hts : t ⊆ s) (hc : t.Countable) (htd : Dense t) (htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t),
    MeasurableSet (Iio a)
⊢ MeasurableSet (Iio a)

Tactic:
rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩

Premises used: Dense.exists_countable_dense_subset_bot_top
-- 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 = ∅ → 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)
neg : ∀ (ha : ∃ b < a, Ioo b a = ∅), MeasurableSet (Iio a)
⊢ MeasurableSet (Iio a)

Tactic:
by_cases! ha : ∀ b < a, (Ioo b a).Nonempty
-- 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 = ∅ → 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
pos : MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)
⊢ MeasurableSet (Iio a)

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

Premises used: MeasurableSet, Set.Icc, 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 = ∅ → 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 : ∀ (y : α), y ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u) y
⊢ Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u

Tactic:
ext y
-- 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 = ∅ → 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 ∈ Iio a ↔ Membership.mem (γ := Set α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc 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 = ∅ → 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
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 = ∅ → 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
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 = ∅ → 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
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 = ∅ → 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
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, hly, hyu.le⟩

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 = ∅ → 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
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, hly, hyu.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 = ∅ → 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 l u : α
hua : u < a
hyu : y ≤ u
⊢ y < a

Tactic:
hyu.trans_lt hua

Premises used: 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 = ∅ → 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 l u : α
hua : u < a
hyu : y ≤ u
⊢ y < a

Tactic:
exact hyu.trans_lt hua

Premises used: 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 = ∅ → 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)

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 = ∅ → 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
pos :
  ∀ (a_1 : α) (ha : a_1 ∈ t) (b : α) (hb : b ∈ t),
    MeasurableSet.{u_5} (α := α) (⋃ (_ : a_1 < b), ⋃ (_ : b < a), Icc a_1 b)
⊢ MeasurableSet.{u_5} (α := α) (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)

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

Premises used: MeasurableSet.biUnion