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 : ℝ
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 μ
pos :
  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))

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
-- 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 μ
⊢ 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:
L1.tendsto_setToL1 hT _ _ ?_

Premises used: MeasureTheory.L1.tendsto_setToL1
-- 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 μ
pos : Tendsto (fun (n : ℕ) ↦ Integrable.toL1 (fs n) ⋯) atTop (𝓝 (Integrable.toL1 f f_int))
⊢ 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:
refine L1.tendsto_setToL1 hT _ _ ?_

Premises used: MeasureTheory.L1.tendsto_setToL1
-- 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 μ
pos : Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ Integrable.toL1 (fs n) ⋯) atTop (𝓝 (Integrable.toL1 f f_int))

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- 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 μ
⊢ 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)
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)

Tactic:
lintegral_norm_tendsto_zero
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ‖Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int‖ = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)

Tactic:
convert! lintegral_norm_tendsto_zero 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
h :
  (∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
⊢ ‖Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int‖ = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal

Tactic:
rw [L1.norm_def]

Premises used: MeasureTheory.L1.norm_def
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
h :
  ∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ =
    ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ
⊢ (∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal

Tactic:
congr 1
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ ∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ =
    ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ) fun (a : α) ↦
    ENNReal.ofReal ‖fs n a - f a‖
⊢ ∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ =
    ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) a‖ₑ)
    fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ) fun (a : α) ↦
    ENNReal.ofReal ‖fs n a - f a‖

Tactic:
rw [← Integrable.toL1_sub]

Premises used: MeasureTheory.Integrable.toL1_sub
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) a‖ₑ)
    fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖

Tactic:
((fs_int n).sub f_int).coeFn_toL1.mono fun x hx => ?_

Premises used: MeasureTheory.Integrable.sub, Filter.EventuallyEq, Filter.Eventually.mono, MeasureTheory.Integrable.coeFn_toL1
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
h :
  ∀ (x : α) (hx : (↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x = (fs n - f) x),
    Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) a‖ₑ) x)
      ((fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖) x)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) a‖ₑ)
    fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖

Tactic:
refine ((fs_int n).sub f_int).coeFn_toL1.mono fun x hx => ?_

Premises used: MeasureTheory.Integrable.sub, Filter.Eventually.mono, MeasureTheory.Integrable.coeFn_toL1
-- 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 μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : (↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x = (fs n - f) x
h : ‖(fs n - f) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
h₁ : ‖(fs n - f) x‖ₑ = ‖fs n x - f x‖ₑ
h₂ h₃ : ‖fs n x - f x‖ₑ = ‖fs n x - f x‖ₑ
⊢ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖

Tactic:
rw [hx, ofReal_norm, Pi.sub_apply]

Premises used: ofReal_norm, Pi.sub_apply
-- 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
rw :
  ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun (n : ι) ↦ setToFun μ T hT (fs n)) l (𝓝 (setToFun μ T hT f))

Tactic:
rw [tendsto_iff_seq_tendsto]

Premises used: Filter.tendsto_iff_seq_tendsto
-- 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
rwa rwa₁ rwa₂ rwa₃ : ∀ (xl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s), ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
rwa [tendsto_atTop'] at xl

Premises used: Filter.tendsto_atTop'
-- 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
have hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s := by rwa [tendsto_atTop'] at xl
-- 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l

Tactic:
have h :
    { x : ι | (fun n => AEStronglyMeasurable (fs n) μ) x } ∩
        { x : ι | (fun n => ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a) x } ∈ l :=
    inter_mem hfs_meas 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
obtain :
  ∀ (k : ℕ)
    (h :
      ∀ b ≥ k,
        Membership.mem (γ := Set ι)
          ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
            {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
          (x b)),
    Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Tactic:
obtain ⟨k, h⟩ := hxl _ h
-- 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
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
rw : Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Tactic:
rw [← tendsto_add_atTop_iff_nat k]

Premises used: Filter.tendsto_add_atTop_iff_nat