-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l.IsCountablyGenerated]
    {F : ι → α → G} {f : α → G} (bound : α → ℝ) (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ)
    (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
    Tendsto (fun n => ∫ a, F n a ∂μ) l (𝓝 <| ∫ a, f a ∂μ)

Proof state:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : CompleteSpace G
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : CompleteSpace G
⊢ Tendsto
    (fun n =>
      if h : True then
        if hf : Integrable (fun a => F n a) μ then L1.integralCLM (Integrable.toL1 (fun a => F n a) hf) else 0
      else 0)
    l
    (𝓝
      (if h : True then
        if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0))

Proof state:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : CompleteSpace G
⊢ Tendsto
    (fun n =>
      if h : True then
        if hf : Integrable (fun a => F n a) μ then L1.integralCLM (Integrable.toL1 (fun a => F n a) hf) else 0
      else 0)
    l
    (𝓝
      (if h : True then
        if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0))

Tactic:
exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
  bound hF_meas h_bound bound_integrable h_lim

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : ¬CompleteSpace G
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
simp [integral, hG, tendsto_const_nhds]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : CompleteSpace G
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))

case neg
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
hG : ¬CompleteSpace G
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))