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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
h : f = fs i - (fs i - f)
⊢ Integrable f μ

Tactic:
convert h'i.sub this

Premises used: MeasureTheory.Integrable.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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ f = fs i - (fs i - f)

Tactic:
abel
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
⊢ Integrable f μ

Tactic:
have hfi : Integrable f μ := by
    obtain ⟨i, hi, h'i⟩ : ∃ i, ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ :=
      (((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists
    have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩
    convert h'i.sub this
    abel
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lp : α →ₘ[μ] E) : α → E)) 1 μ)
    l (𝓝 0)
⊢ Tendsto F_lp l (𝓝 f_lp)

Tactic:
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']

Premises used: MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
simp_rw :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ι) ↦ ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lp : α →ₘ[μ] E) : α → E)) 1 μ)
    l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ι) ↦ ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ) l (𝓝 0)

Tactic:
(tendsto_congr' ?_).mp hfs

Premises used: Iff.mp, Filter.tendsto_congr'
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
refine :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) fun (n : ι) ↦
    ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ι) ↦ ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ) l (𝓝 0)

Tactic:
refine (tendsto_congr' ?_).mp hfs

Premises used: Iff.mp, Filter.tendsto_congr'
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
h :
  ∀ (i : ι) (hi : Integrable (fs i) μ),
    ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ =
      ∫⁻ (x : α), ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ
⊢ l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) fun (n : ι) ↦
    ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ

Tactic:
filter_upwards [hfsi] with i hi
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
⊢ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ

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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖fs i x - f x‖ₑ) fun (x : α) ↦
    ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
⊢ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ

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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
h :
  ∀ (x : α) (hxi : (↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) x = fs i x)
    (hxf : (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E) x = f x),
    ‖fs i x - f x‖ₑ = ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖fs i x - f x‖ₑ) fun (x : α) ↦
    ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ

Tactic:
filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf

Premises used: 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
x : α
hxi : (↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) x = fs i x
hxf : (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E) x = f x
h :
  ‖fs i x - f x‖ₑ =
    ‖(↑(↑(if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0) : α →ₘ[μ] E) : α → E) x -
        (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
h₁ : ‖fs i x - f x‖ₑ = ‖(↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
h₂ : ‖fs i x - f x‖ₑ = ‖fs i x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
h₃ : ‖fs i x - f x‖ₑ = ‖fs i x - (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E) x‖ₑ
⊢ ‖fs i x - f x‖ₑ = ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ

Tactic:
simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]

Premises used: dif_pos
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
⊢ Tendsto F_lp l (𝓝 f_lp)

Tactic:
have tendsto_L1 : Tendsto F_lp l (𝓝 f_lp) := by
    rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
    simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
    refine (tendsto_congr' ?_).mp hfs
    filter_upwards [hfsi] with i hi
    refine lintegral_congr_ae ?_
    filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
    simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
(tendsto_congr' ?_).mp this

Premises used: Iff.mp, Filter.tendsto_congr'
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
refine :
  EventuallyEq.{u_7, u_3} (β := F) l (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) fun (i : ι) ↦
    setToFun μ T hT (fs i)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
refine (tendsto_congr' ?_).mp this

Premises used: Iff.mp, Filter.tendsto_congr'
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
h : ∀ (i : ι) (hi : Integrable (fs i) μ), setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) = setToFun μ T hT (fs i)
⊢ EventuallyEq.{u_7, u_3} (β := F) l (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) fun (i : ι) ↦
    setToFun μ T hT (fs i)

Tactic:
filter_upwards [hfsi] with i hi
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
i : ι
hi : Integrable (fs i) μ
h : (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i
⊢ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) = setToFun μ T hT (fs i)

Tactic:
suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
i : ι
hi : Integrable (fs i) μ
h : (↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i
⊢ (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i

Tactic:
simp_rw [F_lp, dif_pos hi]

Premises used: dif_pos
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
i : ι
hi : Integrable (fs i) μ
⊢ (↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i

Tactic:
hi.coeFn_toL1

Premises used: 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
inr : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f)) by
    refine (tendsto_congr' ?_).mp this
    filter_upwards [hfsi] with i hi
    suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
    simp_rw [F_lp, dif_pos hi]
    exact hi.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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
inr :
  Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l
    (𝓝 (setToFun μ T hT (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E)))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l (𝓝 (setToFun μ T hT f))

Tactic:
rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.Integrable.coeFn_toL1, Filter.EventuallyEq.symm
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l
    (𝓝 (setToFun μ T hT (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E)))

Tactic:
((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1

Premises used: MeasureTheory.continuous_setToFun, dite, Continuous.tendsto, Filter.Tendsto.comp, 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : (i : ι) → ↥(Lp E 1 μ) := fun (i : ι) ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l
    (𝓝 (setToFun μ T hT (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E)))

Tactic:
exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1

Premises used: MeasureTheory.continuous_setToFun, Continuous.tendsto, Filter.Tendsto.comp