awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
rw : r • (↑v : Set α → M) ∅ = 0
⊢ (r • (↑v : Set α → M)) ∅ = 0
have rw₁ : HSMul.hSMul (β := M) r 0 = 0
Tactic: rw [Pi.smul_apply, empty, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
rw : r • (↑v : Set α → M) ∅ = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
⊢ (r • (↑v : Set α → M)) ∅ = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply, empty, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
⊢ (r • (↑v : Set α → M)) x = 0
have rw : r • (↑v : Set α → M) x = 0
Tactic: rw [Pi.smul_apply, v.not_measurable hi, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : r • (↑v : Set α → M) x = 0
⊢ (r • (↑v : Set α → M)) x = 0
have rw₁ : HSMul.hSMul (β := M) r 0 = 0
Tactic: rw [Pi.smul_apply, v.not_measurable hi, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : r • (↑v : Set α → M) x = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
⊢ (r • (↑v : Set α → M)) x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply, v.not_measurable hi, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : IsEmpty α
μ ν : VectorMeasure α M
⊢ μ = ν
have h : ∀ (i : Set α), MeasurableSet i → (↑μ : Set α → M) i = (↑ν : Set α → M) i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : IsEmpty α
μ ν : VectorMeasure α M
i : Set α
h : MeasurableSet i
⊢ (↑μ : Set α → M) i = (↑ν : Set α → M) i
have h : 0 = (↑ν : Set α → M) i
Tactic: rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : IsEmpty α
μ ν : VectorMeasure α M
i : Set α
h_1 : MeasurableSet i
h : 0 = (↑ν : Set α → M) i
⊢ (↑μ : Set α → M) i = (↑ν : Set α → M) i
have h₁ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) x = 0
have rw : (↑v : Set α → M) x + (↑w : Set α → M) x = 0
Tactic: rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x + (↑w : Set α → M) x = 0
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) x = 0
have rw₁ : 0 + (↑w : Set α → M) x = 0
Tactic: rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x + (↑w : Set α → M) x = 0
rw₁ : 0 + (↑w : Set α → M) x = 0
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) x = 0
have rw₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x + (↑w : Set α → M) x = 0
rw₁ : 0 + (↑w : Set α → M) x = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) x = 0
have rw₃ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
⊢ (-(↑v : Set α → M)) x = 0
have rw : -(↑v : Set α → M) x = 0
Tactic: rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : -(↑v : Set α → M) x = 0
⊢ (-(↑v : Set α → M)) x = 0
have rw₁ : (↑v : Set α → M) x = 0
Tactic: rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : -(↑v : Set α → M) x = 0
rw₁ : (↑v : Set α → M) x = 0
⊢ (-(↑v : Set α → M)) x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) x = 0
have rw : (↑v : Set α → M) x - (↑w : Set α → M) x = 0
Tactic: rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x - (↑w : Set α → M) x = 0
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) x = 0
have rw₁ : 0 - (↑w : Set α → M) x = 0
Tactic: rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x - (↑w : Set α → M) x = 0
rw₁ : 0 - (↑w : Set α → M) x = 0
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) x = 0
have rw₂ : HSub.hSub (α := M) 0 0 = 0
Tactic: rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x - (↑w : Set α → M) x = 0
rw₁ : 0 - (↑w : Set α → M) x = 0
rw₂ : HSub.hSub (α := M) 0 0 = 0
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) x = 0
have rw₃ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
have pos : ∀ (hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x),
  HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
Tactic: by_cases hx : x ∈ ⋃ i, f i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
pos :
  ∀ (hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x),
    HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
      (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
have neg : ∀ (hx : x ∉ ⋃ (i : ℕ), f i),
  HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
Tactic: by_cases hx : x ∈ ⋃ i, f i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : x ∉ ⋃ (i : ℕ), f i
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
have hx₁ : ∀ (x_2 : ℕ), x ∉ f x_2
Tactic: simp only [mem_iUnion, not_exists] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
have this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
Tactic: have : MeasurableSet (⋃ i, f i) := by
      apply MeasurableSet.iUnion f_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)
have pos : HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
Tactic: simp only [f_meas, true_and, MeasurableSet.iUnion f_meas, hx, and_self, ↓reduceIte]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
have pos : ∀ (j : ℕ) (hj : x ∈ f j), HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
Tactic: obtain ⟨j, hj⟩ : ∃ j, x ∈ f j := by simpa using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
have pos : HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) (if x ∈ f j then v else 0)
Tactic: nth_rewrite 2 [show v = if x ∈ f j then v else 0 by simp [hj]]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) (if x ∈ f j then v else 0)
have pos : ∀ (b' : ℕ), b' ≠ j → (if x ∈ f b' then v else 0) = 0
Tactic: apply hasSum_single
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
i : ℕ
hi : i ≠ j
⊢ (if x ∈ f i then v else 0) = 0
have this₁ : Disjoint (f i) (f j)
Tactic: have : Disjoint (f i) (f j) := f_disj hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then μ.real (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then μ.real (⋃ (i : ℕ), f i) else 0)
have simp : HasSum (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
  (ENNReal.toReal (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)))
Tactic: simp only [*, MeasurableSet.iUnion hf₁, if_true, measure_iUnion hf₂ hf₁, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (ENNReal.toReal (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)))
have rw : HasSum (α := ℝ) (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
  (∑' (a : ℕ), ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f a)))
Tactic: rw [ENNReal.tsum_toReal_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
rw :
  HasSum (α := ℝ) (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (∑' (a : ℕ), ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f a)))
⊢ HasSum (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (ENNReal.toReal (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)))
have rw₁ : ∀ (a : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [ENNReal.tsum_toReal_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν
have refine_1 : ∀ (h : μ.toSignedMeasure = ν.toSignedMeasure), μ = ν
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
refine_1 : ∀ (h : μ.toSignedMeasure = ν.toSignedMeasure), μ = ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν
have refine_2 : ∀ (h : μ = ν), μ.toSignedMeasure = ν.toSignedMeasure
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
⊢ μ = ν
have refine_1 : ∀ (i : Set α) (hi : MeasurableSet i),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
have rw : (↑ν.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have this : (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
Tactic: have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have refine_1 : ∀ (this : μ.real i = (↑ν.toSignedMeasure : Set α → ℝ) i),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
        measureReal_eq_measureReal_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
refine_1 :
  ∀ (this : μ.real i = (↑ν.toSignedMeasure : Set α → ℝ) i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have refine_1₁ : ∀ (this : μ.real i = ν.real i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
        measureReal_eq_measureReal_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
refine_1 :
  ∀ (this : μ.real i = (↑ν.toSignedMeasure : Set α → ℝ) i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
refine_1₁ :
  ∀ (this : μ.real i = ν.real i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have refine_1₂ : ∀ (this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
        measureReal_eq_measureReal_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure 0) 0
have h : ∀ (i : Set α), MeasurableSet i → (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
have h : (μ + ν).real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
Tactic: rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
h : (μ + ν).real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
have h₁ : μ.real i + ν.real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
Tactic: rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]