awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Iio)) (generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)}))

Tactic:
le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Premises used: Set.mem_range_self, Iff.mpr, Set.singleton_subset_iff, Set.iUnion_subset, Rat.cast, MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range Iio) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Iio)) (generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)}))

Tactic:
refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Premises used: Set.mem_range_self, Iff.mpr, Set.singleton_subset_iff, Set.iUnion_subset, MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
⊢ IsLUB (range Rat.cast ∩ Iio a) a

Tactic:
simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]

Premises used: le_iff_forall_rat_lt_imp_le, isLUB_iff_le_iff, mem_upperBounds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
⊢ IsLUB (range Rat.cast ∩ Iio a) a

Tactic:
have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
    simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
rw : MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio (↑y : ℝ))
⊢ MeasurableSet (Iio a)

Tactic:
rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]

Premises used: Set.image_univ, Set.image_inter_preimage, Set.univ_inter, IsLUB.biUnion_Iio_eq, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
b : ℚ
h : b ∈ Rat.cast ⁻¹' Iio a
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) (Iio (↑b : ℝ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio (↑y : ℝ))

Tactic:
exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range Ioi)) (generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)}))
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)})

Tactic:
rw [borel_eq_generateFrom_Ioi]

Premises used: borel_eq_generateFrom_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Ioi)) (generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)}))

Tactic:
le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Premises used: Set.mem_range_self, Iff.mpr, Set.singleton_subset_iff, Set.iUnion_subset, Rat.cast, MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range Ioi) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Ioi)) (generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)}))

Tactic:
refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Premises used: Set.mem_range_self, Iff.mpr, Set.singleton_subset_iff, Set.iUnion_subset, MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
⊢ IsGLB (range Rat.cast ∩ Ioi a) a

Tactic:
simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]

Premises used: isGLB_iff_le_iff, mem_lowerBounds, le_iff_forall_lt_rat_imp_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
⊢ IsGLB (range Rat.cast ∩ Ioi a) a

Tactic:
have : IsGLB (range ((↑) : ℚ → ℝ) ∩ Ioi a) a := by
    simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
rw : MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi (↑y : ℝ))
⊢ MeasurableSet (Ioi a)

Tactic:
rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]

Premises used: Set.image_univ, Set.image_inter_preimage, Set.univ_inter, IsGLB.biUnion_Ioi_eq, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
b : ℚ
h : b ∈ Rat.cast ⁻¹' Ioi a
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) (Ioi (↑b : ℝ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi (↑y : ℝ))

Tactic:
exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Ioi (b : ℝ)) (by simp)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
rw :
  Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Iic (↑a : ℝ)})

Tactic:
rw [borel_eq_generateFrom_Ioi_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]

Premises used: Real.borel_eq_generateFrom_Ioi_rat, Set.iUnion_singleton_eq_range
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))

Tactic:
le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)) t → MeasurableSet t
refine_2 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Iic (↑a : ℝ)) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
refine_1 : MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ
⊢ MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))

Tactic:
rw [← compl_Iic]

Premises used: Set.compl_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
refine_2 : MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ
⊢ MeasurableSet (α := ℝ) (Iic (↑q : ℝ))

Tactic:
rw [← compl_Ioi]

Premises used: Set.compl_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ
refine_2 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Iic]; rw [← compl_Ioi]]

Premises used: Set.compl_Ioi, Set.compl_Iic, le_antisymm, rfl, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ

Tactic:
MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Premises used: Set.mem_range_self, MeasurableSet.compl, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ

Tactic:
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ

Tactic:
MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Premises used: Set.mem_range_self, MeasurableSet.compl, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ

Tactic:
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
rw :
  Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Ici (↑a : ℝ)})

Tactic:
rw [borel_eq_generateFrom_Iio_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]

Premises used: Real.borel_eq_generateFrom_Iio_rat, Set.iUnion_singleton_eq_range
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))

Tactic:
le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Iio (↑a : ℝ)) t → MeasurableSet t
refine_2 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Ici (↑a : ℝ)) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
refine_1 : MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ
⊢ MeasurableSet (α := ℝ) (Iio (↑q : ℝ))

Tactic:
rw [← compl_Ici]

Premises used: Set.compl_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
refine_2 : MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ
⊢ MeasurableSet (α := ℝ) (Ici (↑q : ℝ))

Tactic:
rw [← compl_Iio]

Premises used: Set.compl_Iio
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ
refine_2 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Ici]; rw [← compl_Iio]]

Premises used: le_antisymm, Set.compl_Iio, Set.compl_Ici, rfl, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ

Tactic:
MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Premises used: Set.mem_range_self, MeasurableSet.compl, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ

Tactic:
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ

Tactic:
MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Premises used: Set.mem_range_self, MeasurableSet.compl, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ

Tactic:
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ IsPiSystem (α := ℝ) {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S}

Tactic:
isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)

Premises used: Rat.cast, isPiSystem_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S}
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})

Tactic:
convert! isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)

Premises used: Rat.cast, isPiSystem_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  ∀ (x : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) x ↔
      Membership.mem (γ := Set (Set ℝ))
        {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S} x
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
x : Set ℝ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ))
      {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S} x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ IsPiSystem (α := ℝ) (Iio '' Rat.cast '' univ)

Tactic:
isPiSystem_image_Iio (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, Rat.cast, isPiSystem_image_Iio, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) (Iio '' Rat.cast '' univ)
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Iio (↑a : ℝ)})

Tactic:
convert! isPiSystem_image_Iio (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, Rat.cast, isPiSystem_image_Iio, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  ∀ (x : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) x ↔
      Membership.mem (γ := Set (Set ℝ)) (Iio '' Rat.cast '' univ) x
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) (Iio '' Rat.cast '' univ)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
x : Set ℝ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Iio '' Rat.cast '' univ) x

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Premises used: Set.image_univ, Set.mem_range, Set.mem_image, Set.iUnion_singleton_eq_range, exists_exists_eq_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ IsPiSystem (α := ℝ) (Ioi '' Rat.cast '' univ)

Tactic:
isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, isPiSystem_image_Ioi, Rat.cast, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) (Ioi '' Rat.cast '' univ)
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Ioi (↑a : ℝ)})

Tactic:
convert! isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, isPiSystem_image_Ioi, Rat.cast, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  ∀ (x : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) x ↔
      Membership.mem (γ := Set (Set ℝ)) (Ioi '' Rat.cast '' univ) x
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) (Ioi '' Rat.cast '' univ)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
x : Set ℝ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Ioi '' Rat.cast '' univ) x

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Premises used: Set.image_univ, Set.mem_range, Set.mem_image, Set.iUnion_singleton_eq_range, exists_exists_eq_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ IsPiSystem (α := ℝ) (Iic '' Rat.cast '' univ)

Tactic:
isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)

Premises used: isPiSystem_image_Iic, Set.univ, Rat.cast, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) (Iic '' Rat.cast '' univ)
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Iic (↑a : ℝ)})

Tactic:
convert! isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)

Premises used: isPiSystem_image_Iic, Set.univ, Rat.cast, Set.image
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  ∀ (x : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) x ↔
      Membership.mem (γ := Set (Set ℝ)) (Iic '' Rat.cast '' univ) x
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) (Iic '' Rat.cast '' univ)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
x : Set ℝ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Iic '' Rat.cast '' univ) x

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Premises used: Set.image_univ, Set.mem_range, Set.mem_image, Set.iUnion_singleton_eq_range, exists_exists_eq_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ IsPiSystem (α := ℝ) (Ici '' Rat.cast '' univ)

Tactic:
isPiSystem_image_Ici (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, Rat.cast, Set.image, isPiSystem_image_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) (Ici '' Rat.cast '' univ)
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Ici (↑a : ℝ)})

Tactic:
convert! isPiSystem_image_Ici (((↑) : ℚ → ℝ) '' univ)

Premises used: Set.univ, Rat.cast, Set.image, isPiSystem_image_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h :
  ∀ (x : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) x ↔
      Membership.mem (γ := Set (Set ℝ)) (Ici '' Rat.cast '' univ) x
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) (Ici '' Rat.cast '' univ)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
x : Set ℝ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Ici '' Rat.cast '' univ) x

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Premises used: Set.image_univ, Set.mem_range, Set.mem_image, Set.iUnion_singleton_eq_range, exists_exists_eq_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
simp :
  ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1),
    Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = Ioo (↑i : ℝ) (↑i_1 : ℝ)
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    (Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    Ioo (↑(-(↑(n + 1) : ℚ)) : ℝ) (↑(HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
refine : -(↑(n + 1) : ℚ) < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
⊢ ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1),
    Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = Ioo (↑i : ℝ) (↑i_1 : ℝ)

Tactic:
refine ⟨-(n + 1 : ℕ), n + 1, ?_, by simp⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
push_cast : -HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
⊢ -(↑(n + 1) : ℚ) < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1

Tactic:
push_cast
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ -HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1

Tactic:
neg_lt_self n.cast_add_one_pos

Premises used: Nat.cast_add_one_pos, neg_lt_self
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ -HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1

Tactic:
exact neg_lt_self n.cast_add_one_pos

Premises used: neg_lt_self
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ ν : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h :
  ∀ (a b : ℚ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
      ((ν : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
simp :
  ∀ (s : Set ℝ),
    (∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1), s = Ioo (↑i : ℝ) (↑i_1 : ℝ)) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ ν : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h :
  ∀ (a b : ℚ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
      ((ν : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
a b : ℚ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
    ((ν : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)

Tactic:
apply h
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable Real.toNNReal

Tactic:
continuous_real_toNNReal.measurable

Premises used: continuous_real_toNNReal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal

Tactic:
measurable_real_toNNReal.comp hf

Premises used: Measurable.comp, measurable_real_toNNReal, NNReal.mk, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ

Tactic:
measurable_real_toNNReal.comp_aemeasurable hf

Premises used: measurable_real_toNNReal, NNReal.mk, Measurable.comp_aemeasurable, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable NNReal.toReal

Tactic:
NNReal.continuous_coe.measurable

Premises used: NNReal.continuous_coe, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (↑(f x) : ℝ)

Tactic:
measurable_coe_nnreal_real.comp hf

Premises used: Measurable.comp, measurable_coe_nnreal_real, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ

Tactic:
measurable_coe_nnreal_real.comp_aemeasurable hf

Premises used: measurable_coe_nnreal_real, Measurable.comp_aemeasurable, NNReal.toReal