awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (Iio a)
have rw : MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio (↑y : ℝ))
Tactic: rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)})
have rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range Ioi)) (generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)}))
Tactic: rw [borel_eq_generateFrom_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Ioi)) (generateFrom (⋃ (a : ℚ), {Ioi (↑a : ℝ)}))
have refine : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range Ioi) t → MeasurableSet t
Tactic: refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
a : ℝ
⊢ MeasurableSet (Ioi a)
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (Ioi a)
have rw : MeasurableSet (α := ℝ) (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi (↑y : ℝ))
Tactic: rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Iic (↑a : ℝ)})
have rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
  (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
Tactic: rw [borel_eq_generateFrom_Ioi_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
have refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)) t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
have refine_2 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Iic (↑a : ℝ)) t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))
have refine_1 : MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ
Tactic: rw [← compl_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iic (↑q : ℝ))
have refine_2 : MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ
Tactic: rw [← compl_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
have refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Iic]; rw [← compl_Ioi]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Iic (↑q : ℝ))ᶜ
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Ioi (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Iic (↑a : ℝ)))
have refine_2 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Ioi (↑q : ℝ))ᶜ
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Iic]; rw [← compl_Ioi]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Ici (↑a : ℝ)})
have rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
  (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
Tactic: rw [borel_eq_generateFrom_Iio_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
have refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Iio (↑a : ℝ)) t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
refine_1 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Iio (↑a : ℝ)) t → MeasurableSet t
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
have refine_2 : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range fun (a : ℚ) ↦ Ici (↑a : ℝ)) t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Iio (↑q : ℝ))
have refine_1 : MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ
Tactic: rw [← compl_Ici]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
q : ℚ
⊢ MeasurableSet (α := ℝ) (Ici (↑q : ℝ))
have refine_2 : MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ
Tactic: rw [← compl_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
have refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Ici]; rw [← compl_Iio]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
refine_1 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Ici (↑q : ℝ))ᶜ
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range fun (a : ℚ) ↦ Iio (↑a : ℝ)))
    (generateFrom (range fun (a : ℚ) ↦ Ici (↑a : ℝ)))
have refine_2 : ∀ (q : ℚ), MeasurableSet (α := ℝ) (Iio (↑q : ℝ))ᶜ
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Ici]; rw [← compl_Iio]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
have h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
  {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S}
Tactic: convert! isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    {S : Set ℝ | ∃ (l : ℚ) (u : ℚ), LT.lt (α := ℝ) (↑l : ℝ) (↑u : ℝ) ∧ Ioo (↑l : ℝ) (↑u : ℝ) = S}
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Iio (↑a : ℝ)})
have h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) (Iio '' Rat.cast '' univ)
Tactic: convert! isPiSystem_image_Iio (((↑) : ℚ → ℝ) '' univ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) (Iio '' Rat.cast '' univ)
have h : ∀ (x : Set ℝ),
  Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iio (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Iio '' Rat.cast '' univ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Ioi (↑a : ℝ)})
have h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) (Ioi '' Rat.cast '' univ)
Tactic: convert! isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) (Ioi '' Rat.cast '' univ)
have h : ∀ (x : Set ℝ),
  Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ioi (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Ioi '' Rat.cast '' univ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Iic (↑a : ℝ)})
have h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) (Iic '' Rat.cast '' univ)
Tactic: convert! isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) (Iic '' Rat.cast '' univ)
have h : ∀ (x : Set ℝ),
  Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Iic '' Rat.cast '' univ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ IsPiSystem (α := ℝ) (⋃ (a : ℚ), {Ici (↑a : ℝ)})
have h : Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) (Ici '' Rat.cast '' univ)
Tactic: convert! isPiSystem_image_Ici (((↑) : ℚ → ℝ) '' univ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) (Ici '' Rat.cast '' univ)
have h : ∀ (x : Set ℝ),
  Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Ici (↑a : ℝ)}) x ↔
    Membership.mem (γ := Set (Set ℝ)) (Ici '' Rat.cast '' univ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    (Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
have simp : ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1),
  Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = Ioo (↑i : ℝ) (↑i_1 : ℝ)
Tactic: simp only [mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1),
    Ioo (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = Ioo (↑i : ℝ) (↑i_1 : ℝ)
have refine : -(↑(n + 1) : ℚ) < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
Tactic: refine ⟨-(n + 1 : ℕ), n + 1, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℕ
⊢ -(↑(n + 1) : ℚ) < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
have push_cast : -HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 < HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ ν : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h :
  ∀ (a b : ℚ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥0∞)
      ((ν : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑a : ℝ) (↑b : ℝ)) : ℝ≥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∞)
have 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∞)
Tactic: simp only [mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ MeasurableMul₂ ℝ≥0∞
have refine_1 : Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).1 * ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).2
Tactic: refine ⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
refine_1 :
  Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).1 * ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).2
⊢ MeasurableMul₂ ℝ≥0∞
have refine_2 : Measurable (β := ℝ≥0∞) fun (r : ℝ≥0) ↦ (∞, (↑r : ℝ≥0∞)).1 * (∞, (↑r : ℝ≥0∞)).2
Tactic: refine ⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
refine_1 :
  Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).1 * ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).2
refine_2 : Measurable (β := ℝ≥0∞) fun (r : ℝ≥0) ↦ (∞, (↑r : ℝ≥0∞)).1 * (∞, (↑r : ℝ≥0∞)).2
⊢ MeasurableMul₂ ℝ≥0∞
have refine_3 : Measurable (β := ℝ≥0∞) fun (r : ℝ≥0) ↦ ((↑r : ℝ≥0∞), ∞).1 * ((↑r : ℝ≥0∞), ∞).2
Tactic: refine ⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ Measurable g
have rcases : ∀ (x : ℕ → ι) (hx : Tendsto x atTop u), Measurable g
Tactic: rcases u.exists_seq_tendsto with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g
have rw : ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))) (x : ℕ → ι) (hx : Tendsto x atTop u), Measurable g
Tactic: rw [tendsto_pi_nhds] at lim
Cleared hypotheses: lim, x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
have h : ∀ (y : α), liminf (fun (n : ℕ) ↦ f (x n) y) atTop = g y
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g
have this : (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
Tactic: have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by
    ext1 y
    exact ((lim y).comp hx).liminf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
⊢ Measurable g
have rw : Measurable (β := ℝ≥0∞) fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
⊢ AEMeasurable g μ
have rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
Tactic: rcases u.exists_seq_tendsto with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ AEMeasurable g μ
have h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
Tactic: have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n ↦ hf (v n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
    a
Tactic: filter_upwards [hlim] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
have h₁ : ∀ (a : α), Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a)) → p a fun (n : ℕ) ↦ f (v n) a
Tactic: filter_upwards [hlim] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
⊢ AEMeasurable g μ
have hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
Tactic: have hp : ∀ᵐ x ∂μ, p x fun n ↦ f (v n) x := by
    filter_upwards [hlim] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ AEMeasurable g μ
have refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
Tactic: refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
⊢ AEMeasurable g μ
have refine_2 : g =ᶠ[ae μ] aeSeqLim
Tactic: refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
⊢ Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
have refine_1 : Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) sorry x else Nonempty.some sorry) atTop
  (𝓝 (if x ∈ aeSeqSet h'f p then g x else sorry.some))
Tactic: simp_rw [aeSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
⊢ Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
have pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) sorry x) atTop (𝓝 (g x))
Tactic: split_ifs with hx