awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp [setToFun, hF]

Premises used: MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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‖ₑ ∂μ
neg : ∀ (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‖ₑ ∂μ

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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‖ₑ ∂μ

Tactic:
simp [setToFun_undef _ hf]

Premises used: MeasureTheory.setToFun_undef
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ
⊢ (↑(NNReal.mk C hC) : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ‖setToFun μ T hT f‖ₑ.toReal ≤ ((↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ₑ ≤ (↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
apply (ENNReal.toReal_le_toReal (by simp)
    (ENNReal.mul_ne_top (by simp) hf.hasFiniteIntegral.ne)).1

Premises used: ENNReal.mul_ne_top, Iff.mp, ENNReal.toReal_le_toReal, MeasureTheory.Integrable.hasFiniteIntegral, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ‖setToFun μ T hT f‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ₑ.toReal ≤ ((↑(NNReal.mk C hC) : ℝ≥0∞) * ∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
simp only [toReal_enorm, toReal_mul, coe_toReal, NNReal.coe_mk]

Premises used: ENNReal.coe_toReal, toReal_enorm, NNReal.coe_mk, ENNReal.toReal_mul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 * ‖Integrable.toL1 f hf‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
apply (norm_setToFun_le hT hf hC).trans

Premises used: LE.le.trans, MeasureTheory.norm_setToFun_le
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ C * ‖Integrable.toL1 f hf‖ ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 pos₁ : (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
rw [Integrable.norm_toL1_eq_lintegral_enorm]

Premises used: MeasureTheory.Integrable.norm_toL1_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg :
  ∀ (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

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg : 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero, NNReal.coe_mk, ofReal_norm]

Premises used: norm_zero, reduceDIte, NNReal.coe_mk, ofReal_norm, MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg :
  ∀ (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

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ
neg : 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp only [setToFun_undef _ hf, norm_zero, NNReal.coe_mk, ofReal_norm]

Premises used: MeasureTheory.setToFun_undef, norm_zero, NNReal.coe_mk, ofReal_norm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ
⊢ 0 ≤ C * (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 * ‖Integrable.toL1 f hf‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ ‖setToFun μ T hT f‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
apply (norm_setToFun_le hT hf hC).trans

Premises used: LE.le.trans, MeasureTheory.norm_setToFun_le
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) : ℝ)
pos₁ : ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ C * ‖Integrable.toL1 f hf‖ ≤ (↑(NNReal.mk C hC) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 ≤ (↑(NNReal.mk C hC) : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 : (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
rw [Integrable.norm_toL1_eq_lintegral_enorm]

Premises used: MeasureTheory.Integrable.norm_toL1_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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))
neg : ∀ (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))

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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))

Tactic:
simp [setToFun, hF]

Premises used: MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ AEStronglyMeasurable f μ

Tactic:
have f_measurable : AEStronglyMeasurable f μ :=
    aestronglyMeasurable_of_tendsto_ae _ fs_measurable h_lim
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 μ
⊢ ∀ (n : ℕ), Integrable (fs n) μ

Tactic:
have fs_int : ∀ n, Integrable (fs n) μ := fun n =>
    bound_integrable.mono' (fs_measurable n) (h_bound _)
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) μ
⊢ Integrable f μ

Tactic:
have f_int : Integrable f μ :=
    ⟨f_measurable,
      hasFiniteIntegral_of_dominated_convergence bound_integrable.hasFiniteIntegral h_bound
        h_lim⟩
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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.{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)

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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) ⋯)
h₁ : setToFun μ T hT f = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
convert! this with n
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
n : ℕ
⊢ setToFun μ T hT (fs n) = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯)

Tactic:
setToFun_eq hT (fs_int n)

Premises used: MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
n : ℕ
⊢ setToFun μ T hT (fs n) = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fs n) ⋯)

Tactic:
exact setToFun_eq hT (fs_int n)

Premises used: MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
⊢ setToFun μ T hT f = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)

Tactic:
setToFun_eq hT f_int

Premises used: MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
⊢ setToFun μ T hT f = (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f f_int)

Tactic:
exact setToFun_eq hT f_int

Premises used: MeasureTheory.setToFun_eq