awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
⊢ ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have neg : ∀ (hf : ¬Integrable f μ), ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have pos : ‖setToFun μ T hT f‖ₑ.toReal ≤ ((↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: apply (ENNReal.toReal_le_toReal (by simp)
    (ENNReal.mul_ne_top (by simp) hf.hasFiniteIntegral.ne)).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖setToFun μ T hT f‖ₑ.toReal ≤ ((↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have pos : ‖setToFun μ T hT f‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: simp only [toReal_enorm, toReal_mul, coe_toReal, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖setToFun μ T hT f‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have pos : C * ‖Integrable.toL1 f hf‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: apply (norm_setToFun_le hT hf hC).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ C * ‖Integrable.toL1 f hf‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have pos : ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have pos : ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
have pos : (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: rw [Integrable.norm_toL1_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos : ∀ (hF : CompleteSpace F), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
pos :
  ∀ (hF : CompleteSpace F), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have neg : ∀ (hF : ¬CompleteSpace F), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : ¬CompleteSpace F
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have neg : 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: simp only [setToFun, hF, ↓reduceDIte, norm_zero, NNReal.coe_mk, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos : ∀ (hf : Integrable f μ), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
pos :
  ∀ (hf : Integrable f μ), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have neg : ∀ (hf : ¬Integrable f μ), ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have neg : 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Tactic: simp only [setToFun_undef _ hf, norm_zero, NNReal.coe_mk, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos : C * ‖Integrable.toL1 f hf‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: apply (norm_setToFun_le hT hf hC).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ C * ‖Integrable.toL1 f hf‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos : C ≤ (↑(NNReal.mk C hC) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
pos : C ≤ (↑(NNReal.mk C hC) : ℝ)
⊢ C * ‖Integrable.toL1 f hf‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos₁ : ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
have pos : (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: rw [Integrable.norm_toL1_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have pos : ∀ (hF : CompleteSpace F), Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
pos : ∀ (hF : CompleteSpace F), Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have neg : ∀ (hF : ¬CompleteSpace F), Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have f_measurable : AEStronglyMeasurable f μ
Tactic: have f_measurable : AEStronglyMeasurable f μ :=
    aestronglyMeasurable_of_tendsto_ae _ fs_measurable h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have fs_int : ∀ (n : ℕ), Integrable (fs n) μ
Tactic: have fs_int : ∀ n, Integrable (fs n) μ := fun n =>
    bound_integrable.mono' (fs_measurable n) (h_bound _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have f_int : Integrable f μ
Tactic: have f_int : Integrable f μ :=
    ⟨f_measurable,
      hasFiniteIntegral_of_dominated_convergence bound_integrable.hasFiniteIntegral h_bound
        h_lim⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
this :
  Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯) : F))
    atTop (𝓝 ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)) : Filter F)
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have h : ∀ (n : ℕ), setToFun μ T hT (fs n) = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) sorry)
Tactic: convert! this with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
this :
  Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯) : F))
    atTop (𝓝 ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)) : Filter F)
h : ∀ (n : ℕ), setToFun μ T hT (fs n) = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯)
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have h₁ : setToFun μ T hT f = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)
Tactic: convert! this with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
have pos : Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) sorry) : F)) atTop
  (𝓝 ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)) : Filter F)
Tactic: suffices
    Tendsto (fun n => L1.setToL1 hT ((fs_int n).toL1 (fs n))) atTop
      (𝓝 (L1.setToL1 hT (f_int.toL1 f))) by
    convert! this with n
    · exact setToFun_eq hT (fs_int n)
    · exact setToFun_eq hT f_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto.{0, u_3} (β := F) (fun (n : ℕ) ↦ ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯) : F))
    atTop (𝓝 ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)) : Filter F)
have pos : Tendsto (fun (n : ℕ) ↦ Integrable.toL1 (fs n) sorry) atTop (𝓝 (Integrable.toL1 f f_int))
Tactic: refine L1.tendsto_setToL1 hT _ _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto (fun (n : ℕ) ↦ Integrable.toL1 (fs n) ⋯) atTop (𝓝 (Integrable.toL1 f f_int))
have pos : Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖Integrable.toL1 (fs e) sorry - Integrable.toL1 f f_int‖) atTop (𝓝 0)
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)
have lintegral_norm_tendsto_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
Tactic: have lintegral_norm_tendsto_zero :
    Tendsto (fun n => ENNReal.toReal <| ∫⁻ a, ENNReal.ofReal ‖fs n a - f a‖ ∂μ) atTop (𝓝 0) :=
    (tendsto_toReal zero_ne_top).comp
      (tendsto_lintegral_norm_of_dominated_convergence fs_measurable
        bound_integrable.hasFiniteIntegral h_bound h_lim)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)
have h : ∀ (n : ℕ), ‖Integrable.toL1 (fs n) sorry - Integrable.toL1 f f_int‖ = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
Tactic: convert! lintegral_norm_tendsto_zero with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ ‖Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int‖ = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
have h : (∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) sorry - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ).toReal =
  (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
Tactic: rw [L1.norm_def]