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
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
simp : Tendsto (fun (n : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))
⊢ Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- 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
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
⊢ Tendsto (fun (n : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
    bound hF_meas h_bound bound_integrable h_lim

Premises used: MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- 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
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
f : α → G
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
⊢ Tendsto (fun (n : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
    bound hF_meas h_bound bound_integrable h_lim

Premises used: MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- 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
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)
⊢ ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a

Tactic:
have hb_nonneg : ∀ᵐ a ∂μ, ∀ n, 0 ≤ bound n a :=
    eventually_countable_forall.2 fun n => (h_bound n).mono fun a => (norm_nonneg _).trans
-- 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
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 : ι
a : α
ha0 : ∀ (n : ι), 0 ≤ bound n a
ha_sum : Summable (α := ℝ) fun (n : ι) ↦ bound n a
⊢ bound n a ≤ ∑' (n : ι), bound n a

Tactic:
ha_sum.le_tsum _ fun i _ => ha0 i

Premises used: Summable.le_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
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 : ι
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (n : ι), 0 ≤ bound n a) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Summable (α := ℝ) fun (n : ι) ↦ bound n a) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ bound n x ≤ (fun (a : α) ↦ (∑' (n : ι), bound n a : ℝ)) x) x} x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (ha0 : ∀ (n : ι), 0 ≤ bound n a) (ha_sum : Summable (α := ℝ) fun (n : ι) ↦ bound n a),
    bound n a ≤ ∑' (n : ι), bound n a
⊢ bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a

Tactic:
filter_upwards [hb_nonneg, bound_summable]
      with _ ha0 ha_sum using ha_sum.le_tsum _ fun i _ => ha0 i
-- 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
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:
have hb_le_tsum : ∀ n, bound n ≤ᵐ[μ] fun a => ∑' n, bound n a := by
    intro n
    filter_upwards [hb_nonneg, bound_summable]
      with _ ha0 ha_sum using ha_sum.le_tsum _ fun i _ => ha0 i
-- 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
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 : ι), Integrable (F n) μ

Tactic:
fun n => bound_integrable.mono' (hF_meas n) ?_

Premises used: MeasureTheory.Integrable.mono'
-- 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
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
refine : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a
⊢ ∀ (n : ι), Integrable (F n) μ

Tactic:
refine fun n => bound_integrable.mono' (hF_meas n) ?_

Premises used: MeasureTheory.Integrable.mono'
-- 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
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:
EventuallyLE.trans (h_bound n) (hb_le_tsum n)

Premises used: Filter.EventuallyLE, Filter.EventuallyLE.trans
-- 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
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)

Premises used: Filter.EventuallyLE.trans
-- 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
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 : ι), Integrable (F n) μ

Tactic:
have hF_integrable : ∀ n, Integrable (F n) μ := by
    refine fun n => bound_integrable.mono' (hF_meas n) ?_
    exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)
-- 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
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) μ
simp :
  Tendsto.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (a : α), f a ∂μ))
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)

Tactic:
simp only [HasSum, ← integral_finsetSum _ fun n _ => hF_integrable n]

Premises used: MeasureTheory.integral_finsetSum, HasSum, SummationFilter.unconditional
-- 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
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.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (a : α), f a ∂μ))

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

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, tsum, SummationFilter.unconditional
-- 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
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) μ
refine_1 :
  ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    AEStronglyMeasurable.{u_1, u_3} (β := G) (fun (a : α) ↦ ∑ i ∈ n, F i a) μ
refine_2 :
  ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ n, F i a) ≤ (fun (a : α) ↦ (∑' (n : ι), bound n a : ℝ)) a
⊢ Tendsto.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (a : α), f a ∂μ))

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

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, tsum, SummationFilter.unconditional
-- 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
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 (SummationFilter.unconditional ι).filter,
    AEStronglyMeasurable.{u_1, u_3} (β := G) (fun (a : α) ↦ ∑ i ∈ n, F i a) μ

Tactic:
Eventually.of_forall fun s => s.aestronglyMeasurable_fun_sum fun n _ => hF_meas n

Premises used: Finset.aestronglyMeasurable_fun_sum, Filter.Eventually.of_forall
-- 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
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 (SummationFilter.unconditional ι).filter,
    AEStronglyMeasurable.{u_1, u_3} (β := G) (fun (a : α) ↦ ∑ i ∈ n, F i a) μ

Tactic:
exact Eventually.of_forall fun s => s.aestronglyMeasurable_fun_sum fun n _ => hF_meas n

Premises used: Filter.Eventually.of_forall
-- 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
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) μ
refine_2 : ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ n, F i a) ≤ (fun (a : α) ↦ (∑' (n : ι), bound n a : ℝ)) a

Tactic:
filter_upwards with s
-- 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
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 ι
h :
  ∀ (a : α) (hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a) (ha0 : ∀ (n : ι), 0 ≤ bound n a)
    (has : Summable (α := ℝ) fun (n : ι) ↦ bound n a), norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a
⊢ ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ 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

Premises used: Iff.mpr, eventually_countable_forall
-- 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
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
⊢ norm.{u_3} (E := G) (∑ n ∈ s, F n a) ≤ ∑ n ∈ s, bound n a

Tactic:
norm_sum_le_of_le _ fun n _ => hFa n

Premises used: norm_sum_le_of_le
-- 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
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
⊢ LE.le (α := ℝ) (∑ n ∈ s, bound n a) (∑' (n : ι), bound n a)

Tactic:
has.sum_le_tsum _ (fun n _ => ha0 n)

Premises used: Summable.sum_le_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
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
⊢ norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a

Tactic:
calc
      ‖∑ n ∈ s, F n a‖ ≤ ∑ n ∈ s, bound n a := norm_sum_le_of_le _ fun n _ => hFa n
      _ ≤ ∑' n, bound n a := has.sum_le_tsum _ (fun n _ => ha0 n)

Premises used: norm_sum_le_of_le, Summable.sum_le_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‖ₑ ∂μ) ∞
pos :
  ∀ (hG : CompleteSpace G), Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
neg :
  ∀ (hG : ¬CompleteSpace G), Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- 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
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.integral
-- 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
⊢ ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ

Tactic:
have hf'' i : AEMeasurable (‖f i ·‖ₑ) μ := (hf i).enorm