awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
pos : ∀ (hf_int : Integrable f μ), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
neg : ∀ (hf_int : ¬Integrable f μ), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
by_cases hf_int : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
hf_int : ¬Integrable f μ
⊢ ¬Integrable f (μ.trim hm)

Tactic:
have hf_int_m : ¬Integrable f (μ.trim hm) := fun hf_int_m =>
      hf_int (integrable_of_integrable_trim hm hf_int_m)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
hf_int : ¬Integrable f μ
hf_int_m : ¬Integrable f (μ.trim hm)
neg : Eq.{u_5 + 1} (α := G) 0 (∫ (x : β), f x ∂μ.trim hm)
neg₁ neg₂ : Eq.{u_5 + 1} (α := G) 0 0
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
rw [integral_undef hf_int, integral_undef hf_int_m]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
hf_int : Integrable f μ
⊢ SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)

Tactic:
haveI : SeparableSpace (range f ∪ {0} : Set G) := hf.separableSpace_range_union_singleton
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)

Tactic:
have hf_seq_meas : ∀ n, StronglyMeasurable[m] (f_seq n) := fun n =>
    @SimpleFunc.stronglyMeasurable β G m _ (f_seq n)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
⊢ ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ

Tactic:
have hf_seq_int : ∀ n, Integrable (f_seq n) μ :=
    SimpleFunc.integrable_approxOn_range (hf.mono hm).measurable hf_int
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
⊢ ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)

Tactic:
have hf_seq_int_m : ∀ n, Integrable (f_seq n) (μ.trim hm) := fun n =>
    (hf_seq_int n).trim hm (hf_seq_meas n)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
⊢ ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)

Tactic:
have hf_seq_eq : ∀ n, ∫ x, f_seq n x ∂μ = ∫ x, f_seq n x ∂μ.trim hm := fun n =>
    integral_trim_simpleFunc hm (f_seq n) (hf_seq_int n)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))

Tactic:
tendsto_integral_of_L1 f hf_int.1 (Eventually.of_forall hf_seq_int) ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, Filter.Eventually.of_forall, And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
refine :
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ) atTop
    (𝓝 0)
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))

Tactic:
refine tendsto_integral_of_L1 f hf_int.1 (Eventually.of_forall hf_seq_int) ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, Filter.Eventually.of_forall, And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ) atTop
    (𝓝 0)

Tactic:
SimpleFunc.tendsto_approxOn_range_L1_enorm (hf.mono hm).measurable hf_int

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ) atTop
    (𝓝 0)

Tactic:
exact SimpleFunc.tendsto_approxOn_range_L1_enorm (hf.mono hm).measurable hf_int

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))

Tactic:
have h_lim_1 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ)) := by
    refine tendsto_integral_of_L1 f hf_int.1 (Eventually.of_forall hf_seq_int) ?_
    exact SimpleFunc.tendsto_approxOn_range_L1_enorm (hf.mono hm).measurable hf_int
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
simp_rw :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))

Tactic:
simp_rw [hf_seq_eq]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))

Tactic:
@tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _
      (Eventually.of_forall hf_seq_int_m) ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, Filter.Eventually.of_forall, And.left, MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
refine :
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ.trim hm)
    atTop (𝓝 0)
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))

Tactic:
refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _
      (Eventually.of_forall hf_seq_int_m) ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, Filter.Eventually.of_forall, And.left, MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ.trim hm)
    atTop (𝓝 0)

Tactic:
@SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable
      (hf_int.trim hm hf)

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ.trim hm)
    atTop (𝓝 0)

Tactic:
exact @SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable
      (hf_int.trim hm hf)

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))

Tactic:
have h_lim_2 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ.trim hm)) := by
    simp_rw [hf_seq_eq]
    refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _
      (Eventually.of_forall hf_seq_int_m) ?_
    exact @SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable
      (hf_int.trim hm hf)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
h_lim_2 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
tendsto_nhds_unique h_lim_1 h_lim_2

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
f_seq : (n : ℕ) → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable.{u_6, u_5} (α := β) (β := G) (⇑(f_seq n) : (a : β) → G)
hf_seq_int : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable.{u_5, u_6} (ε := G) (⇑(f_seq n) : (a : β) → G) (μ.trim hm)
hf_seq_eq :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := G) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) (∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm)
h_lim_1 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
h_lim_2 :
  Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ) atTop
    (𝓝 (∫ (x : β), f x ∂μ.trim hm))
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
exact tendsto_nhds_unique h_lim_1 h_lim_2

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
rw :
  Eq.{u_5 + 1} (α := G) (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ)
    (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_eq_of_ae_eq_trim