-- 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
ι : 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)
inl :
  ∀ (hfsi : ∀ᶠ (i : ι) in ⊥, Integrable (fs i) μ)
    (hfs : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) ⊥ (𝓝 0)),
    Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) ⊥ (𝓝 (setToFun μ T hT f))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
inr₂ inr₃ inr₄ :
  ∀ (hl : l.NeBot) (hfi : Integrable f μ), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
inr₅ :
  ∀ (hl : l.NeBot) (hfi : Integrable f μ),
    let f_lp := Integrable.toL1 f hfi;
    let 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 (fs i)) l (𝓝 (setToFun μ T hT f))
inr₆ :
  ∀ (hl : l.NeBot) (hfi : Integrable f μ),
    let f_lp := Integrable.toL1 f hfi;
    let 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 f))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have inr₇ : ∀ (hl : l.NeBot) (hfi : Integrable f μ),
  let f_lp := Integrable.toL1 f hfi;
  let 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: classical
  rcases eq_or_neBot l with rfl | hl
  · simp
  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
  let f_lp := hfi.toL1 f
  let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0
  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]
  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
  rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
  exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1