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)
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))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have inr : ∀ (hl : l.NeBot), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (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
-- 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))
⊢ Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
have inr₂ : ∀ (hl : l.NeBot) (hfi : Integrable f μ), Tendsto (fun (i : ι) ↦ setToFun μ T hT (fs i)) l (𝓝 (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
-- 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))
⊢ 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 (fs i)) l (𝓝 (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
-- 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))
⊢ 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 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
-- 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
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_6 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n) : (a : α) → E)) atTop
    (𝓝 (setToFun μ T hT f))
have refine : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: refine tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have pos : ∀ (hF : CompleteSpace F), setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
Tactic: by_cases hF : CompleteSpace F
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
pos : ∀ (hF : CompleteSpace F), setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
Tactic: by_cases hF : CompleteSpace F
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have hfi' : Integrable f μ'
Tactic: have hfi' : Integrable f μ' :=
    ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hf).mono_measure hμ'
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
Tactic: have : SeparableSpace (range f ∪ {0} : Set E) := hfm.separableSpace_range_union_singleton
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
have pos : Tendsto (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry n) : (a : β) → E)) atTop
  (𝓝 (setToFun μ T hT (f ∘ φ)))
Tactic: refine tendsto_nhds_unique
    (tendsto_setToFun_approxOn_of_measurable_of_range_subset
      hT' hfm.measurable hfi' _ Subset.rfl) ?_
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n) : (a : β) → E)) atTop
    (𝓝 (setToFun μ T hT (f ∘ φ)))
have h₁ : Eq.{u_3 + 1} (α := ℕ → F)
  (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry n) : (a : β) → E)) fun (n : ℕ) ↦
  setToFun μ T hT (⇑(SimpleFunc.approxOn (f ∘ φ) sorry (range f ∪ {0}) 0 sorry n) : (a : α) → E)
Tactic: convert tendsto_setToFun_approxOn_of_measurable_of_range_subset
    hT (hfm.measurable.comp hφ) hf (range f ∪ {0})
    (union_subset_union_left {0} (range_comp_subset_range φ f)) using 1
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
⊢ Eq.{u_3 + 1} (α := ℕ → F)
    (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n) : (a : β) → E)) fun (n : ℕ) ↦
    setToFun μ T hT (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ n) : (a : α) → E)
have h₁ : ∀ (i : ℕ),
  setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry i) : (a : β) → E) =
    setToFun μ T hT (⇑(SimpleFunc.approxOn (f ∘ φ) sorry (range f ∪ {0}) 0 sorry i) : (a : α) → E)
Tactic: ext i : 1
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
i : ℕ
⊢ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : β) → E) =
    setToFun μ T hT (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : α) → E)
have h₁ : Eq.{u_3 + 1} (α := F)
  (∑ x_1 ∈ (SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry i).range,
    (T' (preimage (β := E) (⇑(SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry i) : (a : β) → E) {x_1}) : (a : E) → F) x_1)
  (∑ x_1 ∈ ((SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry i).comp φ hφ).range,
    (T (preimage (β := E) (⇑((SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry i).comp φ hφ) : (a : α) → E) {x_1}) :
        (a : E) → F)
      x_1)
Tactic: rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
    setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]
-- 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h :
  ∀ (s : Set β) (x_1 : E),
    MeasurableSet s → Eq.{u_3 + 1} (α := F) ((T' s : (a : E) → F) x_1 : F) ((T (φ ⁻¹' s) : (a : E) → F) x_1 : F)
hF : CompleteSpace F
hfi' : Integrable f μ'
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)
i : ℕ
h₁ :
  Eq.{u_3 + 1} (α := F)
    (∑ x_1 ∈ (SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T' (preimage (β := E) (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : β) → E) {x_1}) : (a : E) → F) x_1)
    (∑ x_1 ∈ ((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ).range,
      (T (preimage (β := E) (⇑((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ) : (a : α) → E) {x_1}) :
          (a : E) → F)
        x_1)
⊢ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : β) → E) =
    setToFun μ T hT (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : α) → E)
have h₂ : Integrable.{u_2, u_1} (ε := E) (⇑(SimpleFunc.approxOn (f ∘ φ) sorry (range f ∪ {0}) 0 sorry i) : (a : α) → E) μ
Tactic: rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
    setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]