-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem tendsto_setToFun_of_L1 (hT : DominatedFinMeasAdditive μ T C) {ι} (f : α → E)
    (hfi : Integrable f μ) {fs : ι → α → E} {l : Filter ι} (hfsi : ∀ᶠ i in l, Integrable (fs i) μ)
    (hfs : Tendsto (fun i => ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)) :
    Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 <| setToFun μ T hT f)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(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)) l (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

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

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(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)) l (𝓝 (setToFun μ T hT f))
⊢ (fun i => setToFun μ T hT ↑↑(F_lp i)) =ᶠ[l] fun i => setToFun μ T hT (fs i)

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i => if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
⊢ (fun x => ‖fs i x - f x‖ₑ) =ᶠ[ae μ] fun x => ‖↑↑(F_lp i) x - ↑↑f_lp x‖ₑ

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

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(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) x = fs i x
hxf : ↑↑(Integrable.toL1 f hfi) x = f x
⊢ ‖fs i x - f x‖ₑ = ‖↑↑(F_lp i) x - ↑↑f_lp x‖ₑ

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(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) x - ↑↑f_lp x‖ₑ ∂μ

Tactic:
refine lintegral_congr_ae ?_

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i => if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
i : ι
hi : Integrable (fs i) μ
⊢ (fun x => ‖fs i x - f x‖ₑ) =ᶠ[ae μ] fun x => ‖↑↑(F_lp i) x - ↑↑f_lp x‖ₑ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
⊢ Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hfi : Integrable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i => if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
⊢ Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))