-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
lemma hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι → α → E}
    (hF_int : ∀ i : ι, Integrable (F i) μ) (hF_sum : Summable fun i ↦ ∫ a, ‖F i a‖ ∂μ) :
    HasSum (∫ a, F · a ∂μ) (∫ a, (∑' i, F i a) ∂μ)

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (x : ι), ‖∫ (a : α), ‖F x a‖ ∂μ‖ₑ ≠ ⊤

Tactic:
exact ENNReal.tsum_coe_ne_top_iff_summable.2 <| NNReal.summable_coe.1 hF_sum.abs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ

Tactic:
dsimp [enorm]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ⊤

Tactic:
rw [funext this]

Result:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (x : ι), ‖∫ (a : α), ‖F x a‖ ∂μ‖ₑ ≠ ⊤

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)

Tactic:
exact (hF_sum.of_norm_bounded _ fun i ↦ norm_integral_le_integral_norm _).hasSum

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
simp [integral, hE, hasSum_zero]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊

Tactic:
rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
  Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α), ‖F i a‖ ∂μ)

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ⊤

Tactic:
have (i : ι) : ∫⁻ a, ‖F i a‖ₑ ∂μ = ‖∫ a, ‖F i a‖ ∂μ‖ₑ := by
  dsimp [enorm]
  rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
    Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
  simp only [coe_nnnorm]

Result:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ⊤