awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞

Tactic:
rw [← lintegral_tsum hf''] at hf'

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hf'₁ : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
⊢ CompleteSpace G

Tactic:
rw [← lintegral_tsum hf''] at hf'

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hf'₁ : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG₁ : CompleteSpace G
⊢ ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ

Tactic:
rw [← lintegral_tsum hf''] at hf'

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)

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

Premises used: Filter.Eventually.mono, MeasureTheory.ae_lt_top', AEMeasurable.tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
refine : ∀ (x : α), LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞ → Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)
⊢ ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)

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

Premises used: Filter.Eventually.mono, MeasureTheory.ae_lt_top', AEMeasurable.tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
x : α
hx : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞
rw : Ne (α := ℝ≥0∞) (∑' (a : ι), (↑‖f a x‖₊ : ℝ≥0∞)) ∞
⊢ Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)

Tactic:
rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]

Premises used: ENNReal.tsum_coe_ne_top_iff_summable_coe
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
x : α
hx : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞
⊢ Ne (α := ℝ≥0∞) (∑' (a : ι), (↑‖f a x‖₊ : ℝ≥0∞)) ∞

Tactic:
hx.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
x : α
hx : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞
⊢ Ne (α := ℝ≥0∞) (∑' (a : ι), (↑‖f a x‖₊ : ℝ≥0∞)) ∞

Tactic:
exact hx.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)

Tactic:
have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) := by
    rw [← lintegral_tsum hf''] at hf'
    refine (ae_lt_top' (AEMeasurable.tsum hf'') hf').mono ?_
    intro x hx
    rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
    exact hx.ne
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (b : ι), ∫ (a : α), f b a ∂μ)

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

Premises used: NNNorm.nnnorm, MeasureTheory.hasSum_integral_of_dominated_convergence, HasSum.tsum_eq, And.intro, Eq.symm, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
pos : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
pos₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
pos₂ : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
pos₃ : ∀ᵐ (a : α) ∂μ, HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n a) (∑' (i : ι), f i a)
⊢ Eq.{u_3 + 1} (α := G) (∫ (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

Premises used: NNNorm.nnnorm, MeasureTheory.hasSum_integral_of_dominated_convergence, HasSum.tsum_eq, And.intro, Eq.symm, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
n : ι
pos : ∀ (x : α), ‖f n x‖ ≤ ‖f n x‖
⊢ ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a

Tactic:
filter_upwards with x
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
n : ι
x : α
⊢ ‖f n x‖ ≤ ‖f n x‖

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (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) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
pos : ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ < ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ

Tactic:
dsimp [HasFiniteIntegral]

Premises used: MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
rwa : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
rwa₁ rwa₂ rwa₃ rwa₄ : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
⊢ ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞

Tactic:
rwa [lintegral_tsum hf'', lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (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]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (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:
this
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
h : ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ
⊢ ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ < ∞

Tactic:
convert! this using 1
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ enorm (E := ℝ) (∑' (n : ι), ‖f n a‖)) fun (a : α) ↦
    ∑' (n : ι), ‖f n a‖ₑ
⊢ ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞)) fun (a : α) ↦
    ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ enorm (E := ℝ) (∑' (n : ι), ‖f n a‖)) fun (a : α) ↦
    ∑' (n : ι), ‖f n a‖ₑ

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_tsum, enorm_eq_nnnorm, NNReal.nnnorm_eq]

Premises used: enorm_eq_nnnorm, coe_nnnorm, NNReal.nnnorm_eq, NNReal.coe_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
h :
  ∀ (a : α) (ha : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)),
    (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞) = ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞)) fun (a : α) ↦
    ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)

Tactic:
filter_upwards [hhh] with a ha
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (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‖₊) : ℝ≥0∞) = ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)

Tactic:
ENNReal.coe_tsum (NNReal.summable_coe.mp ha)

Premises used: NNReal.summable_coe, ENNReal.coe_tsum, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (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‖₊) : ℝ≥0∞) = ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)

Tactic:
exact ENNReal.coe_tsum (NNReal.summable_coe.mp ha)

Premises used: NNReal.summable_coe, ENNReal.coe_tsum, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
h :
  ∀ (x : α) (hx : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)),
    HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n x) (∑' (i : ι), f i x)
⊢ ∀ᵐ (a : α) ∂μ, HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n a) (∑' (i : ι), f i a)

Tactic:
filter_upwards [hhh] with x hx
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
x : α
hx : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n x) (∑' (i : ι), f i x)

Tactic:
hx.of_norm.hasSum

Premises used: Summable.of_norm, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
x : α
hx : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n x) (∑' (i : ι), f i x)

Tactic:
exact hx.of_norm.hasSum

Premises used: Summable.of_norm, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
pos :
  ∀ (hE : CompleteSpace E),
    HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
neg :
  ∀ (hE : ¬CompleteSpace E),
    HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
simp [integral, hE, hasSum_zero]

Premises used: hasSum_zero, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
pos : HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)
pos₁ : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ) ∞
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
rw [integral_tsum (fun i ↦ (hF_int i).1)]

Premises used: And.left, MeasureTheory.integral_tsum
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)

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

Premises used: Summable.hasSum, Summable.of_norm_bounded
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum.{u_2, u_4} (α := E) (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

Premises used: Summable.hasSum, Summable.of_norm_bounded
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
rw : ENNReal.ofReal (∫ (a : α), (↑‖F i a‖₊ : ℝ) ∂μ) = ENNReal.ofReal (∫ (x : α), ‖F i x‖ ∂μ)
⊢ ∫⁻ (a : α), (↑‖F i a‖₊ : ℝ≥0∞) ∂μ = (↑(nnnorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)) : ℝ≥0∞)

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)))]

Premises used: MeasureTheory.integral_nonneg, coe_nnnorm, ENNReal.coe_nnreal_eq, norm_nonneg, MeasureTheory.lintegral_coe_eq_integral, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : 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 (∫ (x : α), ‖F i x‖ ∂μ)

Tactic:
simp only [coe_nnnorm]

Premises used: coe_nnnorm