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
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
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
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
refine : ∫⁻ (x : X), ‖f x‖ₑ ∂ν < (↑ε : ℝ≥0∞)
⊢ (↑(nndist.{u_3} (α := E) (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
          (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) :
      ℝ≥0∞) <
    (↑ε : ℝ≥0∞)

Tactic:
refine (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt ?_

Premises used: MeasureTheory.nndist_integral_add_measure_le_lintegral, And.right, And.left, LE.le.trans_lt
-- 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
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
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν <
    ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)

Tactic:
rw [← hν, lintegral_add_measure, lintegral_finsetSum_measure] at hs

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.lintegral_finsetSum_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
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
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
hs₁ :
  ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν <
    ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
⊢ @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν

Tactic:
rw [← hν, lintegral_add_measure, lintegral_finsetSum_measure] at hs

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.lintegral_finsetSum_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
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
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
hs₁ :
  ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν <
    ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
hf₁ : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
⊢ ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
rw [← hν, lintegral_add_measure, lintegral_finsetSum_measure] at hs

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.lintegral_finsetSum_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
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 ι
ν : Measure X
hs :
  ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν <
    ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < (↑ε : ℝ≥0∞)

Tactic:
lt_of_add_lt_add_left hs

Premises used: lt_of_add_lt_add_left
-- 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
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 ι
ν : Measure X
hs :
  ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν <
    ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
hf : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < (↑ε : ℝ≥0∞)

Tactic:
exact lt_of_add_lt_add_left hs

Premises used: lt_of_add_lt_add_left
-- 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 μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂Measure.sum μ) (∑' (i : ι), ∫ (x : X), f x ∂μ i)

Tactic:
(hasSum_integral_measure hf).tsum_eq.symm

Premises used: HasSum.tsum_eq, MeasureTheory.hasSum_integral_measure, Eq.symm
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
pos :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))),
    Eq.{u_3 + 1} (α := E)
      (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
        fun (x : X) ↦ f x)
      (∑' (i : ι), (c i).toReal • f (x i))
neg :
  ∀
    (hf :
      ¬@Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))),
    Eq.{u_3 + 1} (α := E)
      (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
        fun (x : X) ↦ f x)
      (∑' (i : ι), (c i).toReal • f (x i))
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
      fun (x : X) ↦ f x)
    (∑' (i : ι), (c i).toReal • f (x i))

Tactic:
by_cases hf : Integrable f (.sum (fun i ↦ (c i) • .dirac (x i)))

Premises used: MeasureTheory.Integrable, HSMul.hSMul, MeasureTheory.Measure.sum
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
pos :
  Eq.{u_3 + 1} (α := E) (∑' (i : ι), ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
    (∑' (i : ι), (c i).toReal • f (x i))
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
      fun (x : X) ↦ f x)
    (∑' (i : ι), (c i).toReal • f (x i))

Tactic:
rw [integral_sum_measure hf]

Premises used: MeasureTheory.integral_sum_measure
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
pos : ∀ (i : ι), ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)) = (c i).toReal • f (x i)
⊢ Eq.{u_3 + 1} (α := E) (∑' (i : ι), ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
    (∑' (i : ι), (c i).toReal • f (x i))

Tactic:
congr with i
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
i : ι
pos :
  HSMul.hSMul (β := E) (c i).toReal (@integral _ _ _ _ mX (Measure.dirac (x i)) fun (x : X) ↦ f x) =
    (c i).toReal • f (x i)
pos₁ pos₂ : (c i).toReal • f (x i) = (c i).toReal • f (x i)
⊢ ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)) = (c i).toReal • f (x i)

Tactic:
rw [integral_smul_measure, integral_dirac]

Premises used: MeasureTheory.integral_dirac, MeasureTheory.integral_smul_measure
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬@Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
neg : ¬Summable.{u_3, u_1} (α := E) fun (i : ι) ↦ (c i).toReal • f (x i)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
      fun (x : X) ↦ f x)
    (∑' (i : ι), (c i).toReal • f (x i))

Tactic:
rw [integral_undef hf, tsum_eq_zero_of_not_summable]

Premises used: MeasureTheory.integral_undef, tsum_eq_zero_of_not_summable
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬@Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
neg : ¬Summable (α := ℝ) fun (x_1 : ι) ↦ ‖(c x_1).toReal • f (x x_1)‖
⊢ ¬Summable.{u_3, u_1} (α := E) fun (i : ι) ↦ (c i).toReal • f (x i)

Tactic:
apply mt Summable.norm

Premises used: mt, Summable.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
f : X → E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
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:
mt (integrable_sum_dirac hc) hf

Premises used: mt, MeasureTheory.integrable_sum_dirac
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬@Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
h : ∀ (x_1 : ι), ‖(c x_1).toReal • f (x x_1)‖ = (c x_1).toReal * ‖f (x x_1)‖
⊢ ¬Summable (α := ℝ) fun (x_1 : ι) ↦ ‖(c x_1).toReal • f (x x_1)‖

Tactic:
convert! mt (integrable_sum_dirac hc) hf

Premises used: mt, MeasureTheory.integrable_sum_dirac
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬@Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
x_1 : ι
⊢ ‖(c x_1).toReal • f (x x_1)‖ = (c x_1).toReal * ‖f (x x_1)‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : CompleteSpace E
hc : ∀ (i : ι), c i ≠ ∞
hf : Summable (α := ℝ) fun (i : ι) ↦ (c i).toReal * ‖f (x i)‖
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ (c i).toReal • f (x i))
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
      fun (x : X) ↦ f x)

Tactic:
simpa using hasSum_integral_measure (integrable_sum_dirac hc hf)

Premises used: MeasureTheory.hasSum_integral_measure, MeasureTheory.integrable_sum_dirac
-- 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 : NormedSpace ℝ E
inst_3 : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst_4 : CompleteSpace E
hc : ∀ (i : ι), c i ≠ ∞
hf : Summable (α := ℝ) fun (i : ι) ↦ (c i).toReal * ‖f (x i)‖
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)))
      fun (x : X) ↦ f x)
    (∑' (i : ι), (c i).toReal • f (x i))

Tactic:
(hasSum_integral_sum_dirac hc hf).tsum_eq.symm

Premises used: HasSum.tsum_eq, Eq.symm, MeasureTheory.hasSum_integral_sum_dirac
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
inst_4 : Countable X
hf : Integrable f μ
⊢ @Integrable _ _ _ _ mX f
    (Measure.sum fun (a : X) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))

Tactic:
rw [← Measure.sum_smul_dirac μ] at hf

Premises used: MeasureTheory.Measure.sum_smul_dirac
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
inst_4 : Countable X
hf :
  @Integrable _ _ _ _ mX f
    (Measure.sum fun (a : X) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
rw :
  Eq.{u_3 + 1} (α := E)
    (∑' (i : X),
      ∫ (x : X), f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {i} : ℝ≥0∞) (Measure.dirac i))
    (∑' (x : X),
      Measure.real (α := X) (m := mX)
          (Measure.sum fun (a : X) ↦
            HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
          {x} •
        f x)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∑' (x : X), μ.real {x} • f x)

Tactic:
rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]

Premises used: MeasureTheory.Measure.sum_smul_dirac, MeasureTheory.integral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
inst_4 : Countable X
hf :
  @Integrable _ _ _ _ mX f
    (Measure.sum fun (a : X) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
e_f :
  ∀ (a : X),
    ∫ (x : X), f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a) =
      Measure.real (α := X) (m := mX)
          (Measure.sum fun (a : X) ↦
            HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
          {a} •
        f a
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (i : X),
      ∫ (x : X), f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {i} : ℝ≥0∞) (Measure.dirac i))
    (∑' (x : X),
      Measure.real (α := X) (m := mX)
          (Measure.sum fun (a : X) ↦
            HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
          {x} •
        f x)

Tactic:
congr 1 with a : 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
f : X → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
inst_4 : Countable X
hf :
  @Integrable _ _ _ _ mX f
    (Measure.sum fun (a : X) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
a : X
e_f :
  HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}))
      (@integral _ _ _ _ mX (Measure.dirac a) fun (x : X) ↦ f x) =
    Measure.real (α := X) (m := mX)
        (Measure.sum fun (a : X) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
        {a} •
      f a
e_f₁ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a =
    Measure.real (α := X) (m := mX)
        (Measure.sum fun (a : X) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
        {a} •
      f a
e_f₂ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a = μ.real {a} • f a
e_f₃ e_f₄ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a = ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a
⊢ ∫ (x : X), f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a) =
    Measure.real (α := X) (m := mX)
        (Measure.sum fun (a : X) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) ((μ : (a : Set X) → ℝ≥0∞) {a} : ℝ≥0∞) (Measure.dirac a))
        {a} •
      f a

Tactic:
rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]

Premises used: MeasureTheory.Measure.sum_smul_dirac, MeasureTheory.integral_dirac, MeasureTheory.measureReal_def, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
⊢ Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }

Tactic:
have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
rw :
  ∀
    (hf :
      @Integrable _ _ _ { x : X // x ∈ s } (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
        (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
hg :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f
        (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    AEStronglyMeasurable (m₀ := mX) f
      (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
hf₁ :
  ∀
    (hf :
      @Integrable _ _ _ _ mX f
        (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
          (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)))
    (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }),
    AEMeasurable (α := { x : X // x ∈ s }) (_m := Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
      (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
hs₁ : ∀ (hf : Integrable f (μ.restrict s)) (hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }), MeasurableSet s
⊢ @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)

Tactic:
rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf

Premises used: MeasureTheory.IntegrableOn, map_comap_subtype_coe, MeasureTheory.integrable_map_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf :
  @Integrable _ _ _ { x : X // x ∈ s } (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
⊢ @Integrable.{u_3, u_2} E _ _ _ (Subtype.instMeasurableSpace (p := fun (x : X) ↦ x ∈ s))
    (fun (x : (↑s : Type u_2)) ↦ f (↑x : X)) (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ)

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf :
  @Integrable _ _ _ _ mX f
    (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))
hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
⊢ AEStronglyMeasurable (m₀ := mX) f
    (Measure.map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ))

Tactic:
Integrable.aestronglyMeasurable hf

Premises used: MeasureTheory.Integrable.aestronglyMeasurable