-- 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 h.e'_3.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‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ⊤
⊢ (fun a => ↑(∑' (a_1 : ι), ‖f a_1 a‖₊)) =ᶠ[ae μ] fun a => ∑' (n : ι), ↑‖f n a‖₊

Tactic:
filter_upwards [hhh] with a ha

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‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ⊤
a : α
ha : Summable fun n => ↑‖f n a‖₊
⊢ ↑(∑' (a_1 : ι), ‖f a_1 a‖₊) = ∑' (n : ι), ↑‖f 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
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:
rwa [lintegral_tsum hf'', lt_top_iff_ne_top]

Result:
no goals

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

Tactic:
exact hx.ne

Result:
no goals

Proof state:
case pos.convert_3.hf.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‖₊
⊢ ∀ (i : ι), AEMeasurable (fun x => ‖f i x‖₊) μ

Tactic:
exact fun i => (hf i).nnnorm.aemeasurable

Result:
no goals

Proof state:
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‖₊
⊢ AEMeasurable (fun a => ↑(∑' (a_1 : ι), ‖f a_1 a‖₊)) μ

Tactic:
apply AEMeasurable.coe_nnreal_real

Result:
case pos.convert_3.hf
α : 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‖₊
⊢ AEMeasurable (fun x => ∑' (a : ι), ‖f a x‖₊) μ

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

Tactic:
intro x hx

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

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

Tactic:
refine (ae_lt_top' (AEMeasurable.ennreal_tsum hf'') hf').mono ?_

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

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‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ⊤

Tactic:
convert this using 1

Result:
case h.e'_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‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ

Proof state:
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)

Tactic:
exact hx.of_norm.hasSum

Result:
no goals

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

Tactic:
rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]

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