-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → α → G} {f : α → G}
    (bound : ι → α → ℝ) (hF_meas : ∀ n, AEStronglyMeasurable (F n) μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound n a)
    (bound_summable : ∀ᵐ a ∂μ, Summable fun n => bound n a)
    (bound_integrable : Integrable (fun a => ∑' n, bound n a) μ)
    (h_lim : ∀ᵐ a ∂μ, HasSum (fun n => F n a) (f a)) :
    HasSum (fun n => ∫ a, F n a ∂μ) (∫ a, f a ∂μ)

Proof state:
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ Tendsto (fun s => ∫ (a : α), ∑ i ∈ s, F i a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
refine tendsto_integral_filter_of_dominated_convergence
    (fun a => ∑' n, bound n a) ?_ ?_ bound_integrable h_lim

Result:
case refine_1
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ ∀ᶠ (n : Finset ι) in atTop, AEStronglyMeasurable (fun a => ∑ i ∈ n, F i a) μ

case refine_2
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ᵐ (a : α) ∂μ, ‖∑ i ∈ n, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a

Proof state:
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a

Tactic:
intro n

Result:
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
n : ι
⊢ bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a

Proof state:
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
n : ι
⊢ ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a

Tactic:
exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)

Result:
no goals

Proof state:
case refine_2.h
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
s : Finset ι
⊢ ∀ᵐ (a : α) ∂μ, ‖∑ i ∈ s, F i a‖ ≤ ∑' (n : ι), bound n a

Tactic:
filter_upwards [eventually_countable_forall.2 h_bound, hb_nonneg, bound_summable]
  with a hFa ha0 has

Result:
case h
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a
bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
s : Finset ι
a : α
hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a
ha0 : ∀ (n : ι), 0 ≤ bound n a
has : Summable fun n => bound n a
⊢ ‖∑ i ∈ s, F i a‖ ≤ ∑' (n : ι), bound n a