-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_trim (hm : m ≤ m0) {f : β → G} (hf : StronglyMeasurable[m] f) :
    ∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
haveI : SeparableSpace (range f ∪ {0} : Set G) := hf.separableSpace_range_union_singleton

Result:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Proof state:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto (fun i => ∫⁻ (x : β), ‖(f_seq i) x - f x‖ₑ ∂μ.trim hm) atTop (𝓝 0)

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

Result:
no goals

Proof state:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

case neg
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : ¬Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
swap

Result:
case neg
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : ¬Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Proof state:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
⊢ Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))

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

Result:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
⊢ Tendsto (fun i => ∫⁻ (x : β), ‖(f_seq i) x - f x‖ₑ ∂μ) atTop (𝓝 0)

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
h_lim_2 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ.trim hm))
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
exact tendsto_nhds_unique h_lim_1 h_lim_2

Result:
no goals

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
borelize G

Result:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.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)

Result:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : 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✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm