awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hl : l.NeBot
⊢ Integrable f μ
have obtain : ∀ (i : ι) (hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1) (h'i : Integrable (fs i) μ), Integrable f μ
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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) μ
⊢ Integrable f μ
have this : Integrable (fs i - f) μ
Tactic: have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩
-- 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)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ Integrable f μ
have h : f = fs i - (fs i - f)
Tactic: convert h'i.sub this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have hfi : 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
-- 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)
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)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lp : α →ₘ[μ] E) : α → E)) 1 μ) l
  (𝓝 0)
Tactic: rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
-- 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)
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 : ι) ↦ eLpNorm ((↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lp : α →ₘ[μ] E) : α → E)) 1 μ)
    l (𝓝 0)
have simp_rw : Tendsto (β := ℝ≥0∞)
  (fun (n : ι) ↦ ∫⁻ (x : α), ‖(↑(↑(F_lp n) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ) l (𝓝 0)
Tactic: simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
-- 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)
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)
have 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‖ₑ ∂μ
Tactic: refine (tendsto_congr' ?_).mp hfs
-- 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)
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
⊢ 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‖ₑ ∂μ
have h : ∀ (i : ι) (hi : Integrable (fs i) μ),
  ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ ∂μ
Tactic: filter_upwards [hfsi] with i hi
-- 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)
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‖ₑ ∂μ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖fs i x - f x‖ₑ) fun (x : α) ↦
  ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
Tactic: refine lintegral_congr_ae ?_
-- 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)
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) μ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖fs i x - f x‖ₑ) fun (x : α) ↦
    ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
have 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‖ₑ
Tactic: filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
-- 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)
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‖ₑ
⊢ ‖fs i x - f x‖ₑ = ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
have h₁ : ‖fs i x - f x‖ₑ = ‖(↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
Tactic: simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
-- 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)
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‖ₑ
⊢ ‖fs i x - f x‖ₑ = ‖(↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
have h₂ : ‖fs i x - f x‖ₑ = ‖fs i x - (↑(↑f_lp : α →ₘ[μ] E) : α → E) x‖ₑ
Tactic: simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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 (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have tendsto_L1 : 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]
-- 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)
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))
have 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)
Tactic: refine (tendsto_congr' ?_).mp this
-- 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)
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))
⊢ EventuallyEq.{u_7, u_3} (β := F) l (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) fun (i : ι) ↦
    setToFun μ T hT (fs i)
have h : ∀ (i : ι) (hi : Integrable (fs i) μ), setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) = setToFun μ T hT (fs i)
Tactic: filter_upwards [hfsi] with i hi
-- 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)
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) μ
⊢ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) = setToFun μ T hT (fs i)
have h : (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i
Tactic: suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
-- 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)
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) μ
⊢ (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i
have h : (↑(↑(Integrable.toL1 (fs i) hi) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fs i
Tactic: simp_rw [F_lp, dif_pos hi]
-- 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)
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 (fs i)) l (𝓝 (setToFun μ T hT f))
have inr : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) 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
-- 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)
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 f))
have inr : Tendsto (fun (i : ι) ↦ setToFun μ T hT (↑(↑(F_lp i) : α →ₘ[μ] E) : α → E)) l
  (𝓝 (setToFun μ T hT (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] E) : α → E)))
Tactic: rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
-- 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)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have 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))
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
Cleared hypotheses: l, hfsi, hfs