awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
h₁ : ∀ (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) ∞

Tactic:
convert! h.tsum_ofReal_lt_top with i

Premises used: Summable.tsum_ofReal_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
h₁ : ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i
h₂ : (ae (μ i)).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ ‖f a‖
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

Tactic:
simp_rw [ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
x : X
⊢ LE.le (α := ℝ) (0 x) ((fun (a : X) ↦ ‖f a‖) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ (ae (μ i)).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ ‖f a‖

Tactic:
exact ae_of_all _ fun _ ↦ by positivity

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ Summable (α := ℝ) fun (x : ι) ↦ (∫⁻ (x : X), ‖f x‖ₑ ∂μ x).toReal

Tactic:
ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_

Premises used: ENNReal.summable_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
h : ∀ (i : ι), ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal
convert! : Ne (α := ℝ≥0∞) (∑' (x : ι), (fun (i : ι) ↦ ∫⁻ (x : X), ‖f x‖ₑ ∂μ i) x) ∞
⊢ Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i

Tactic:
convert! ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i

Premises used: ENNReal.summable_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ ∀ᵐ (x : X) ∂μ i, ‖f x‖ₑ < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
h : Eq (α := ℝ) (∫ (x : X), ‖f x‖ ∂μ i) (∫ (a : X), ‖f a‖ₑ.toReal ∂μ i)
rw : AEMeasurable (β := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) (μ i)
⊢ ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal

Tactic:
rw [← integral_toReal ?_ (by simp)]

Premises used: MeasureTheory.integral_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ Eq (α := ℝ) (∫ (x : X), ‖f x‖ ∂μ i) (∫ (a : X), ‖f a‖ₑ.toReal ∂μ i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) (μ i)

Tactic:
(hf.aestronglyMeasurable.mono_measure (Measure.le_sum _ i)).enorm

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.le_sum, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) (μ i)

Tactic:
exact (hf.aestronglyMeasurable.mono_measure (Measure.le_sum _ i)).enorm

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.le_sum, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
rw : ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∑' (x : ι), (fun (i : ι) ↦ ∫⁻ (x : X), ‖f x‖ₑ ∂μ i) x) ∞

Tactic:
rw [← lintegral_sum_measure]

Premises used: MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞

Tactic:
hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞

Tactic:
exact hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
f : X → E
inst_2 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hc : ∀ (i : ι), c i ≠ ∞
h : Summable (α := ℝ) fun (i : ι) ↦ (c i).toReal * ‖f (x i)‖
i : ι
⊢ ‖f (x i)‖ₑ < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
f : X → E
inst_2 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hc : ∀ (i : ι), c i ≠ ∞
h : Summable (α := ℝ) fun (i : ι) ↦ (c i).toReal * ‖f (x i)‖
⊢ Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i))

Tactic:
simpa using h
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hf : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
⊢ Summable (α := ℝ) fun (i : ι) ↦ (c i).toReal * ‖f (x i)‖

Tactic:
simpa using hf.summable_integral

Premises used: MeasureTheory.Integrable.summable_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
⊢ ∀ (i : ι), Integrable f (μ i)

Tactic:
have hfi : ∀ i, Integrable f (μ i) := fun i ↦ hf.mono_measure (Measure.le_sum _ _)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
simp :
  Tendsto.{u_1, u_3} (β := E) (fun (s : Finset ι) ↦ @integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (x : X), f x ∂Measure.sum μ))
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : X), f x ∂μ i) (∫ (x : X), f x ∂Measure.sum μ)

Tactic:
simp only [HasSum, ← integral_finsetSum_measure fun i _ ↦ hfi i]

Premises used: MeasureTheory.integral_finsetSum_measure, HasSum, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (s : Finset ι) ↦ @integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (x : X), f x ∂Measure.sum μ))

Tactic:
Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
refine :
  ∀ (ε : ℝ) (ε0 : 0 < ε),
    ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
      Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ε)
        (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (s : Finset ι) ↦ @integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (x : X), f x ∂Measure.sum μ))

Tactic:
refine Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ ε

Tactic:
ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ
ε0 : 0 < ε
lift :
  ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)),
    ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
      Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
        (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ε)
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)

Tactic:
lift ε to ℝ≥0 using ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞

Tactic:
have hf_lt : (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < ∞ := hf.2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)

Tactic:
tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)

Premises used: Set.Mem, Filter.tendsto_id, ENNReal.lt_add_right, tendsto_const_nhds, Filter.Eventually, setOf, Set.preimage, Filter.Tendsto.add, lt_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
refine_1 : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ ≠ ∞
refine_2 : (↑ε : ℝ≥0∞) ≠ 0
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)

Tactic:
refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)

Premises used: Filter.tendsto_id, ENNReal.lt_add_right, tendsto_const_nhds, Filter.Tendsto.add, lt_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ ≠ ∞

Tactic:
hf_lt.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ (↑ε : ℝ≥0∞) ≠ 0

Tactic:
ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', Iff.mp, NNReal.coe_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ ≠ ∞

Tactic:
exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]

Premises used: Iff.mpr, ENNReal.coe_ne_zero, LT.lt.ne', Iff.mp, NNReal.coe_ne_zero, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)

Tactic:
have hmem : ∀ᶠ y in 𝓝 (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ), (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < y + ε := by
    refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
    exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)

Tactic:
((hasSum_lintegral_measure (fun x ↦ ‖f x‖ₑ) μ).eventually hmem).mono fun s hs ↦ ?_

Premises used: MeasureTheory.hasSum_lintegral_measure, Filter.Eventually.mono, ENorm.enorm, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
refine :
  ∀ (s : Finset ι)
    (hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)),
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)

Tactic:
refine ((hasSum_lintegral_measure (fun x ↦ ‖f x‖ₑ) μ).eventually hmem).mono fun s hs ↦ ?_

Premises used: MeasureTheory.hasSum_lintegral_measure, Filter.Eventually.mono, ENorm.enorm, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
⊢ ∃ (ν : Measure X), ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩

Premises used: Exists.intro, MeasureTheory.Measure.sum, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
refine :
  HAdd.hAdd (α := Measure X) (∑ i ∈ s, μ i) (Measure.sum fun (i : (↑(↑s : Set ι)ᶜ : Type u_1)) ↦ μ (↑i : ι)) =
    Measure.sum μ
⊢ ∃ (ν : Measure X), ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
⊢ HAdd.hAdd (α := Measure X) (∑ i ∈ s, μ i) (Measure.sum fun (i : (↑(↑s : Set ι)ᶜ : Type u_1)) ↦ μ (↑i : ι)) =
    Measure.sum μ

Tactic:
simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ

Premises used: MeasureTheory.Measure.sum_add_sum_compl, SetLike.coe, MeasureTheory.Measure.sum_coe_finset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
obtain :
  ∀ (ν : Measure X) (hν : ∑ i ∈ s, μ i + ν = Measure.sum μ),
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
⊢ Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
    (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)

Tactic:
obtain ⟨ν, hν⟩ : ∃ ν, (∑ i ∈ s, μ i) + ν = Measure.sum μ := by
    refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩
    simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ

Premises used: MeasureTheory.Measure.sum, Finset.sum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
rw :
  (↑(nndist.{u_3} (α := E) (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
          (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) :
      ℝ≥0∞) <
    (↑ε : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
    (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)

Tactic:
rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν]

Premises used: coe_nndist, ENNReal.coe_lt_coe, Metric.mem_ball, NNReal.coe_lt_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν

Tactic:
rw [← hν, integrable_add_measure] at hf

Premises used: MeasureTheory.integrable_add_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
hf₁ : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
⊢ ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
rw [← hν, integrable_add_measure] at hf

Premises used: MeasureTheory.integrable_add_measure