-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem integral_tsum {ι} [Countable ι] {f : ι → α → G} (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (hf' : ∑' i, ∫⁻ a : α, ‖f i a‖ₑ ∂μ ≠ ∞) :
    ∫ a : α, ∑' i, f i a ∂μ = ∑' i, ∫ a : α, f i a ∂μ

Proof state:
case pos.convert_4
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ HasFiniteIntegral (fun a => ∑' (n : ι), (fun i a => ↑‖f i a‖₊) n a) μ

Tactic:
dsimp [HasFiniteIntegral]

Result:
case pos.convert_4
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ⊤

Proof state:
case pos.convert_5
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∀ᵐ (a : α) ∂μ, HasSum (fun n => f n a) (∑' (i : ι), f i a)

Tactic:
filter_upwards [hhh] with x hx

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
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
x : α
hx : Summable fun n => ↑‖f n x‖₊
⊢ HasSum (fun n => f n x) (∑' (i : ι), f i x)

Proof state:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

Tactic:
have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) := by
  rw [← lintegral_tsum hf''] at hf'
  refine (ae_lt_top' (AEMeasurable.ennreal_tsum hf'') hf').mono ?_
  intro x hx
  rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
  exact hx.ne

Result:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

Tactic:
convert (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh
        ⟨_, _⟩ _).tsum_eq.symm

Result:
case pos.convert_2
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun i a => ↑‖f i a‖₊) n a

case pos.convert_3
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ AEStronglyMeasurable (fun a => ∑' (n : ι), (fun i a => ↑‖f i a‖₊) n a) μ

case pos.convert_4
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ HasFiniteIntegral (fun a => ∑' (n : ι), (fun i a => ↑‖f i a‖₊) n a) μ

case pos.convert_5
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∀ᵐ (a : α) ∂μ, HasSum (fun n => f n a) (∑' (i : ι), f i a)

Proof state:
case neg
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos.convert_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
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
n : ι
x : α
⊢ ‖f n x‖ ≤ ↑‖f n x‖₊

Tactic:
rfl

Result:
no goals

Proof state:
case pos.convert_4
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ⊤

Tactic:
have : ∫⁻ a, ∑' n, ‖f n a‖ₑ ∂μ < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]

Result:
case pos.convert_4
α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ⊤