-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem tendsto_integral_approxOn_of_measurable [MeasurableSpace E] [BorelSpace E] {f : α → E}
    {s : Set E} [SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f)
    (hs : ∀ᵐ x ∂μ, f x ∈ closure s) {y₀ : E} (h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) :
    Tendsto (fun n => (SimpleFunc.approxOn f hfm s y₀ h₀ n).integral μ)
      atTop (𝓝 <| ∫ x, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable (fun x => y₀) μ
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
have hfi' := SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i

Result:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable (fun x => y₀) μ
hfi' : ∀ (n : ℕ), Integrable (⇑(approxOn f hfm s y₀ h₀ n)) μ
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable (fun x => y₀) μ
hfi' : ∀ (n : ℕ), Integrable (⇑(approxOn f hfm s y₀ h₀ n)) μ
⊢ Tendsto
    (fun n =>
      if h : True then
        if hf : Integrable (fun x => (approxOn f hfm s y₀ h₀ n) x) μ then
          L1.integralCLM (Integrable.toL1 (fun x => (approxOn f hfm s y₀ h₀ n) x) hf)
        else 0
      else 0)
    atTop
    (𝓝
      (if h : True then
        if hf : Integrable (fun x => f x) μ then L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0
      else 0))

Tactic:
exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ)
  hfi hfm hs h₀ h₀i

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable (fun x => y₀) μ
hfi' : ∀ (n : ℕ), Integrable (⇑(approxOn f hfm s y₀ h₀ n)) μ
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, hE, L1.integral]

Result:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable (fun x => y₀) μ
hfi' : ∀ (n : ℕ), Integrable (⇑(approxOn f hfm s y₀ h₀ n)) μ
⊢ Tendsto
    (fun n =>
      if h : True then
        if hf : Integrable (fun x => (approxOn f hfm s y₀ h₀ n) x) μ then
          L1.integralCLM (Integrable.toL1 (fun x => (approxOn f hfm s y₀ h₀ n) x) hf)
        else 0
      else 0)
    atTop
    (𝓝
      (if h : True then
        if hf : Integrable (fun x => f x) μ then L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0
      else 0))