awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g 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 neg : ∀ (hx : x ∉ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ Nonempty.some sorry) atTop (𝓝 sorry.some)
Tactic: split_ifs with 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∞
μ : 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 : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))
have pos : Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))
Tactic: simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f 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∞
μ : 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
set set₁ : AEMeasurable g μ
⊢ AEMeasurable g μ
have refine_1 : let aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else sorry.some;
∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
Tactic: classical
  set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
  refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
  · unfold aeSeqLim
    simp_rw [aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
    · exact tendsto_const_nhds
  · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
-- 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
set set₁ : AEMeasurable g μ
refine_1 :
  let 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 (𝓝 (aeSeqLim x))
⊢ AEMeasurable g μ
have refine_2 : let aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else sorry.some;
g =ᶠ[ae μ] aeSeqLim
Tactic: classical
  set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
  refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
  · unfold aeSeqLim
    simp_rw [aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
    · exact tendsto_const_nhds
  · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∑' (i : ι), f i x
have simp_rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x
Tactic: simp_rw [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) (∑' (i : ι), f i)
have h₁ : ∀ (x : α), Eq (α := ℝ≥0∞) ((∑' (i : ι), f i) x) (∑' (i : ι), f i x)
Tactic: convert! Measurable.ennreal_tsum h with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ ∑' (i : ι), f i x
have simp_rw : Measurable (β := ℝ≥0) fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))
Tactic: simp_rw [NNReal.tsum_eq_toNNReal_tsum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ι), f i x) μ
have simp_rw : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x) μ
Tactic: simp_rw [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_5
x : MeasurableSpace α
ι : Type u_6
inst : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ∑' (i : ι), f i x) μ
have simp_rw : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))) μ
Tactic: simp_rw [NNReal.tsum_eq_toNNReal_tsum]
-- 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 simp_rw : ∀ (hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(g x) : ℝ≥0∞)
Tactic: simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢
Cleared hypotheses: hf
-- 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
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(g x) : ℝ≥0∞)
have refine : Tendsto.{u_5, u_1} (β := α → ℝ≥0∞) (fun (i : ι) (x : α) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 fun (x : α) ↦ (↑(g x) : ℝ≥0∞))
Tactic: refine ENNReal.measurable_of_tendsto' u hf ?_
-- 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
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
⊢ Tendsto.{u_5, u_1} (β := α → ℝ≥0∞) (fun (i : ι) (x : α) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 fun (x : α) ↦ (↑(g x) : ℝ≥0∞))
have rw : ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x)))
  (hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)) (x : α),
  Tendsto (fun (i : ι) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 (↑(g x) : ℝ≥0∞))
Tactic: rw [tendsto_pi_nhds] at lim ⊢
Cleared hypotheses: lim, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable f
have refine_1 : Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)
Tactic: refine measurable_of_real_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
refine_1 : Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)
⊢ Measurable f
have refine_2 : Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊥, x)
Tactic: refine measurable_of_real_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
refine_1 : Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)
refine_2 : Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊥, x)
⊢ Measurable f
have refine_3 : Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊤, x)
Tactic: refine measurable_of_real_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)
have refine_1 : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦
  ((fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)) ∘ Prod.swap) ((↑p.1 : EReal), p.2)
Tactic: refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
⊢ Measurable (β := EReal) fun (x : EReal) ↦ c * x
have refine : Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
Tactic: refine measurable_of_measurable_real ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
⊢ Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
have h : ∀ (p : ℝ), ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥
Tactic: ext p
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
p : ℝ
⊢ ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥
have pos : ∀ (h1 : p = 0), ⊥ * (↑p : EReal) = 0
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
p : ℝ
pos : ∀ (h1 : p = 0), ⊥ * (↑p : EReal) = 0
⊢ ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥
have pos₁ : ∀ (h1 : ¬p = 0) (h2 : p < 0), ⊥ * (↑p : EReal) = ⊤
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
p : ℝ
pos : ∀ (h1 : p = 0), ⊥ * (↑p : EReal) = 0
pos₁ : ∀ (h1 : ¬p = 0) (h2 : p < 0), ⊥ * (↑p : EReal) = ⊤
⊢ ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥
have neg : ∀ (h1 : ¬p = 0) (h2 : ¬p < 0), ⊥ * (↑p : EReal) = ⊥
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : p < 0
⊢ ⊥ * (↑p : EReal) = ⊤
have pos : Eq (α := EReal) ⊤ ⊤
Tactic: rw [bot_mul_coe_of_neg h2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ ⊥ * (↑p : EReal) = ⊥
have neg : 0 < p
Tactic: rw [bot_mul_coe_of_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
c : EReal
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
have h1 : Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
Tactic: have h1 : (fun (p : ℝ) ↦ (⊥ : EReal) * p)
      = fun p ↦ if p = 0 then (0 : EReal) else (if p < 0 then ⊤ else ⊥) := by
    ext p
    split_ifs with h1 h2
    · simp [h1]
    · rw [bot_mul_coe_of_neg h2]
    · rw [bot_mul_coe_of_pos]
      exact lt_of_le_of_ne (not_lt.mp h2) (Ne.symm h1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
have refine : Measurable (β := EReal) fun (p : ℝ) ↦ if p < 0 then ⊤ else ⊥
Tactic: refine Measurable.piecewise (measurableSet_singleton _) measurable_const ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
have h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
Tactic: have h2 : Measurable fun (p : ℝ) ↦ if p = 0 then (0 : EReal) else if p < 0 then ⊤ else ⊥ := by
    refine Measurable.piecewise (measurableSet_singleton _) measurable_const ?_
    exact Measurable.piecewise measurableSet_Iio measurable_const measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ ⊤ * (↑p : EReal)
have top : Measurable (β := EReal) fun (p : ℝ) ↦ -(⊥ * (↑p : EReal))
Tactic: simp_rw [← neg_bot, neg_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ -(⊥ * (↑p : EReal))
have top : Measurable (β := EReal) fun (x : ℝ) ↦ ⊥ * (↑x : EReal)
Tactic: apply Measurable.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
have bot : Measurable (β := EReal) fun (p : ℝ) ↦ ⊥ * (↑p : EReal)
Tactic: induction c with
  | bot => rwa [h1]
  | coe c => exact (measurable_id.const_mul _).coe_real_ereal
  | top =>
    simp_rw [← neg_bot, neg_mul]
    apply Measurable.neg
    rwa [h1]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
bot : Measurable (β := EReal) fun (p : ℝ) ↦ ⊥ * (↑p : EReal)
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
have coe : ∀ (c : ℝ), Measurable (β := EReal) fun (p : ℝ) ↦ (↑c : EReal) * (↑p : EReal)
Tactic: induction c with
  | bot => rwa [h1]
  | coe c => exact (measurable_id.const_mul _).coe_real_ereal
  | top =>
    simp_rw [← neg_bot, neg_mul]
    apply Measurable.neg
    rwa [h1]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
bot : Measurable (β := EReal) fun (p : ℝ) ↦ ⊥ * (↑p : EReal)
coe : ∀ (c : ℝ), Measurable (β := EReal) fun (p : ℝ) ↦ (↑c : EReal) * (↑p : EReal)
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
have top : Measurable (β := EReal) fun (p : ℝ) ↦ ⊤ * (↑p : EReal)
Tactic: induction c with
  | bot => rwa [h1]
  | coe c => exact (measurable_id.const_mul _).coe_real_ereal
  | top =>
    simp_rw [← neg_bot, neg_mul]
    apply Measurable.neg
    rwa [h1]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ MeasurableMul₂ EReal
have refine_1 : Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
Tactic: refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
refine_1 :
  Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
⊢ MeasurableMul₂ EReal
have refine_2 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2
Tactic: refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
refine_1 :
  Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
refine_2 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2
⊢ MeasurableMul₂ EReal
have refine_3 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2
Tactic: refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
refine_1 :
  Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
refine_2 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2
refine_3 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2
⊢ MeasurableMul₂ EReal
have refine_4 : Measurable (β := EReal) fun (r : ℝ) ↦ ((↑r : EReal), ⊥).1 * ((↑r : EReal), ⊥).2
Tactic: refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
refine_1 :
  Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
refine_2 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2
refine_3 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2
refine_4 : Measurable (β := EReal) fun (r : ℝ) ↦ ((↑r : EReal), ⊥).1 * ((↑r : EReal), ⊥).2
⊢ MeasurableMul₂ EReal
have refine_5 : Measurable (β := EReal) fun (r : ℝ) ↦ ((↑r : EReal), ⊤).1 * ((↑r : EReal), ⊤).2
Tactic: refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
have h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (n : ℕ), norm_sets n) x ↔ Membership.mem (γ := Set α) univ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
x : α
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), norm_sets n) x ↔ Membership.mem (γ := Set α) univ x
have h : ∃ (i : ℕ), x ∈ norm_sets i
Tactic: simp only [Set.mem_iUnion, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, f x ≤ (↑n : ℝ≥0)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
have norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
Tactic: have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ := by
    ext1 x
    simp only [Set.mem_iUnion, Set.mem_univ, iff_true]
    exact exists_nat_ge (f x)