awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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∞)
⊢ Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
    (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
have 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)
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 ι) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 μ
⊢ Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
    (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
have rw : (↑(nndist.{u_3} (α := E) (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) :
    ℝ≥0∞) <
  (↑ε : ℝ≥0∞)
Tactic: rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
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 μ
⊢ (↑(nndist.{u_3} (α := E) (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
          (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) :
      ℝ≥0∞) <
    (↑ε : ℝ≥0∞)
have hf₁ : @Integrable _ _ _ _ mX f (∑ i ∈ s, μ i) ∧ Integrable f ν
Tactic: rw [← hν, integrable_add_measure] at hf
Cleared hypotheses: hf, hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 μ
⊢ (↑(nndist.{u_3} (α := E) (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
          (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) :
      ℝ≥0∞) <
    (↑ε : ℝ≥0∞)
have refine : ∫⁻ (x : X), ‖f x‖ₑ ∂ν < (↑ε : ℝ≥0∞)
Tactic: refine (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
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 μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < (↑ε : ℝ≥0∞)
have hs₁ : ∑ 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
Cleared hypotheses: hs, hf, hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 ≠ ∞
⊢ 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))
have 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))
Tactic: by_cases hf : Integrable f (.sum (fun i ↦ (c i) • .dirac (x i)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases hf : Integrable f (.sum (fun i ↦ (c i) • .dirac (x i)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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)))
⊢ 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))
have 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))
Tactic: rw [integral_sum_measure hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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)))
⊢ 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))
have pos : ∀ (i : ι), ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)) = (c i).toReal • f (x i)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 : ι
⊢ ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)) = (c i).toReal • f (x i)
have pos : HSMul.hSMul (β := E) (c i).toReal (@integral _ _ _ _ mX (Measure.dirac (x i)) fun (x : X) ↦ f x) =
  (c i).toReal • f (x i)
Tactic: rw [integral_smul_measure, integral_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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)
⊢ ∫ (x : X), f x ∂HSMul.hSMul (β := Measure X) (c i) (Measure.dirac (x i)) = (c i).toReal • f (x i)
have pos₁ : (c i).toReal • f (x i) = (c i).toReal • f (x i)
Tactic: rw [integral_smul_measure, integral_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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)))
⊢ 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))
have neg : ¬Summable.{u_3, u_1} (α := E) fun (i : ι) ↦ (c i).toReal • f (x i)
Tactic: rw [integral_undef hf, tsum_eq_zero_of_not_summable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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.{u_3, u_1} (α := E) fun (i : ι) ↦ (c i).toReal • f (x i)
have neg : ¬Summable (α := ℝ) fun (x_1 : ι) ↦ ‖(c x_1).toReal • f (x x_1)‖
Tactic: apply mt Summable.norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 (x_1 : ι) ↦ ‖(c x_1).toReal • f (x x_1)‖
have h : ∀ (x_1 : ι), ‖(c x_1).toReal • f (x x_1)‖ = (c x_1).toReal * ‖f (x x_1)‖
Tactic: convert! mt (integrable_sum_dirac hc) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
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 μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∑' (x : X), μ.real {x} • f x)
have hf₁ : @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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∑' (x : X), μ.real {x} • f x)
have 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)
Tactic: rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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))
⊢ 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)
have 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
Tactic: congr 1 with a : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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
⊢ ∫ (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
have 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
Tactic: rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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
⊢ ∫ (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
have 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
Tactic: rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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
⊢ ∫ (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
have e_f₂ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a = μ.real {a} • f a
Tactic: rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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
⊢ ∫ (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
have e_f₃ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a = ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) {a}) • f a
Tactic: rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
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 μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∑' (x : (↑s : Type u_2)), μ.real {(↑x : X)} • f (↑x : X))
have hi : Countable.{max 1 (u_2 + 1)} { x : X // x ∈ s }
Tactic: have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
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 }
⊢ @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)) μ)
have 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)) μ)
Tactic: rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
Cleared hypotheses: hf, hi