awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
⊢ μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x =
    (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x
have e_f : ENNReal.toReal ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x =
  ENNReal.toReal ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x
Tactic: simp only [measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
⊢ ENNReal.toReal ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x =
    ENNReal.toReal ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x
have e_f : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
  ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have pos : ∀ (hG : CompleteSpace G), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
pos : ∀ (hG : CompleteSpace G), 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)
have neg : ∀ (hG : ¬CompleteSpace G), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have pos : ∀ (hf_int : Integrable f μ), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
Tactic: by_cases hf_int : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have neg : ∀ (hf_int : ¬Integrable f μ), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
Tactic: by_cases hf_int : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have hf_int_m : ¬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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have neg : Eq.{u_5 + 1} (α := G) 0 (∫ (x : β), f x ∂μ.trim hm)
Tactic: rw [integral_undef hf_int, integral_undef hf_int_m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have neg₁ : Eq.{u_5 + 1} (α := G) 0 0
Tactic: rw [integral_undef hf_int, integral_undef hf_int_m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have this : SeparableSpace.{u_5} (↑(range f ∪ {0}) : Type u_5)
Tactic: haveI : SeparableSpace (range f ∪ {0} : Set G) := hf.separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 ⋯
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have hf_seq_meas : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have hf_seq_int : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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) μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have hf_seq_int_m : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have 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)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ∂μ))
have refine : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ) atTop
  (𝓝 0)
Tactic: refine tendsto_integral_of_L1 f hf_int.1 (Eventually.of_forall hf_seq_int) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have h_lim_1 : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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))
have simp_rw : Tendsto.{0, u_5} (β := G) (fun (n : ℕ) ↦ ∫ (x : β), (f_seq n : (a : β) → G) x ∂μ.trim hm) atTop
  (𝓝 (∫ (x : β), f x ∂μ.trim hm))
Tactic: simp_rw [hf_seq_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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))
have refine : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := G) ((f_seq i : (a : β) → G) x : G) (f x)‖ₑ ∂μ.trim hm)
  atTop (𝓝 0)
Tactic: refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _
      (Eventually.of_forall hf_seq_int_m) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 ∂μ))
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have h_lim_2 : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
have rw : Eq.{u_5 + 1} (α := G) (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ)
  (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm)
Tactic: rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have pos : ∀ (hr : r = 0),
  eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
pos :
  ∀ (hr : r = 0),
    eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have neg : ∀ (hr : ¬r = 0),
  eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have rw : eLpNorm (ε := ℝ) 0 1 μ ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
rw :
  eLpNorm (ε := ℝ) 0 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have rw₁ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
rw :
  eLpNorm (ε := ℝ) 0 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₁ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have rw₂ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑0 : ℝ≥0∞)
Tactic: rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
rw :
  eLpNorm (ε := ℝ) 0 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₁ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₂ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑0 : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have rw₃ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * 0
Tactic: rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
rw :
  eLpNorm (ε := ℝ) 0 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₁ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₂ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑0 : ℝ≥0∞)
rw₃ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have rw₄ : LE.le (α := ℝ≥0∞) 0 0
Tactic: rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have pos : f =ᶠ[ae μ] 0
Tactic: suffices f =ᵐ[μ] 0 by
      rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
⊢ f =ᶠ[ae μ] 0
have hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑0 : ℝ)
Tactic: rw [hr] at hf
Cleared hypotheses: hf, hr