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
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
f : α → E
s : Set E
inst_6 : SeparableSpace.{u_2} (↑s : Type u_2)
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ y₀) μ
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (⇑(SimpleFunc.approxOn f hfm s y₀ h₀ n) : (a : α) → E)) atTop
    (𝓝 (setToFun μ T hT f))

Tactic:
tendsto_setToFun_of_L1 hT _ hfi.aestronglyMeasurable
    (Eventually.of_forall (SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i))
    (SimpleFunc.tendsto_approxOn_L1_enorm hfm _ hs (hfi.sub h₀i).2)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.sub, Filter.Eventually.of_forall, And.right, MeasureTheory.SimpleFunc.integrable_approxOn, MeasureTheory.tendsto_setToFun_of_L1, MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
G : Type u_5
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup F'
inst_5 : NormedSpace ℝ F'
inst_6 : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f_1 g : α → E
hT : DominatedFinMeasAdditive μ T C
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_9 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- 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
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))

Tactic:
tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)

Premises used: MeasureTheory.integrable_zero, MeasureTheory.tendsto_setToFun_approxOn_of_measurable
-- 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
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
refine : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ T hT (⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n) : (a : α) → E)) atTop
    (𝓝 (setToFun μ T hT f))

Tactic:
refine tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)

Premises used: MeasureTheory.integrable_zero, MeasureTheory.tendsto_setToFun_approxOn_of_measurable
-- 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
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
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Premises used: Set.mem_range_self, subset_closure, Filter.Eventually.of_forall, Set.mem_union_left, Singleton.singleton, OfNat.ofNat
-- 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
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
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Premises used: Set.mem_range_self, subset_closure, Filter.Eventually.of_forall, Set.mem_union_left, Singleton.singleton, OfNat.ofNat
-- 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 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 ∘ φ)
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- 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 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 ∘ φ)

Tactic:
simp [setToFun, hF]

Premises used: 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 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
⊢ Integrable f μ'

Tactic:
have hfi' : Integrable f μ' :=
    ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hf).mono_measure hμ'
-- 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 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 μ'
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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 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
⊢ SeparableSpace.{u_2} (↑(range f ∪ {0}) : Type u_2)

Tactic:
have : SeparableSpace (range f ∪ {0} : Set E) := hfm.separableSpace_range_union_singleton
-- 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 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 ∘ φ)

Tactic:
tendsto_nhds_unique
    (tendsto_setToFun_approxOn_of_measurable_of_range_subset
      hT' hfm.measurable hfi' _ Subset.rfl) ?_

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, Set.Subset.rfl, tendsto_nhds_unique
-- 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 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)
pos :
  Tendsto (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n) : (a : β) → E)) atTop
    (𝓝 (setToFun μ T hT (f ∘ φ)))
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
refine tendsto_nhds_unique
    (tendsto_setToFun_approxOn_of_measurable_of_range_subset
      hT' hfm.measurable hfi' _ Subset.rfl) ?_

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, Set.Subset.rfl, tendsto_nhds_unique
-- 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 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 ∘ φ)))

Tactic:
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))

Premises used: Set.range_comp_subset_range, Measurable.comp, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, Set.union_subset_union_left, Set.range, Union.union, Singleton.singleton, OfNat.ofNat
-- 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 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)
h₁ :
  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)
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ' T' hT' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n) : (a : β) → E)) atTop
    (𝓝 (setToFun μ T hT (f ∘ φ)))

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

Premises used: Set.range_comp_subset_range, Measurable.comp, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, Set.union_subset_union_left, Set.range, Union.union, Singleton.singleton, OfNat.ofNat
-- 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 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)
h₁ :
  ∀ (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)
⊢ 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)

Tactic:
ext i : 1
-- 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 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)
h₂ : Integrable.{u_2, u_1} (ε := E) (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : α) → E) μ
⊢ 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)

Tactic:
rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
    setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]

Premises used: MeasureTheory.SimpleFunc.approxOn_comp, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.setToFun_simpleFunc, MeasureTheory.SimpleFunc.integrable_approxOn_range
-- 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 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 : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- 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 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 : ℕ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ 0) μ

Tactic:
simp
-- 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 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 : ℕ
⊢ Integrable.{u_2, u_1} (ε := E) (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) : (a : α) → E) μ

Tactic:
apply SimpleFunc.integrable_approxOn _ hf (by simp) (by simp)

Premises used: MeasureTheory.SimpleFunc.integrable_approxOn
-- 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 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 ⋯ (insert 0 (range f)) 0 ⋯ i).range,
      (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {x_1}) :
          (a : E) → F)
        x_1)
    (∑ x_1 ∈ ((SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).comp φ hφ).range,
      (T (preimage (β := E) ((⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) : (a : β) → E) ∘ φ) {x_1}) :
          (a : E) → F)
        x_1)
⊢ 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)

Tactic:
simp only [union_singleton, SimpleFunc.measurableSet_preimage, h, ← preimage_comp,
    SimpleFunc.coe_comp]

Premises used: Set.preimage_comp, MeasureTheory.SimpleFunc.measurableSet_preimage, MeasureTheory.SimpleFunc.coe_comp, Set.union_singleton