awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
w : VectorMeasure α M
measureOf' : Set α → M
empty' : measureOf' ∅ = 0
not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0
m_iUnion' :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf' (f i)) (measureOf' (⋃ (i : ℕ), f i))
h :
  (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
          VectorMeasure α M } :
      Set α → M) =
    (↑w : Set α → M)
⊢ { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
      VectorMeasure α M } =
    w
have mk : ∀ (measureOf'_1 : Set α → M) (empty'_1 : measureOf'_1 ∅ = 0)
  (not_measurable'_1 : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'_1 i = 0)
  (m_iUnion'_1 :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf'_1 (f i)) (measureOf'_1 (⋃ (i : ℕ), f i)))
  (h :
    (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
            VectorMeasure α M } :
        Set α → M) =
      (↑{ measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1,
            m_iUnion' := m_iUnion'_1 : VectorMeasure α M } :
        Set α → M)),
  { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
      VectorMeasure α M } =
    { measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1, m_iUnion' := m_iUnion'_1 }
Tactic: cases w
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
have rw : (↑v : Set α → M) = (↑w : Set α → M) ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: rw [← coe_injective.eq_iff, funext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
rw : (↑v : Set α → M) = (↑w : Set α → M) ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ v = w ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
have rw₁ : (∀ (x : Set α), (↑v : Set α → M) x = (↑w : Set α → M) x) ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: rw [← coe_injective.eq_iff, funext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
have mp : v = w → ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
mp : v = w → ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
have mpr : (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) → v = w
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) → v = w
have mpr : (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) →
  ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: rw [ext_iff']
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i
have pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i
have neg : ∀ (hi : ¬MeasurableSet i), (↑v : Set α → M) i = (↑w : Set α → M) i
Tactic: by_cases hi : MeasurableSet 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))
have rcases : ∀ (e : β → ℕ) (he : Function.Injective e),
  HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))
Tactic: rcases Countable.exists_injective_nat β with ⟨e, he⟩
-- 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))
have rw : HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
Tactic: rw [← hasSum_extend_zero he]
-- 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
have h : ∀ (x : ℕ),
  Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
    (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)
Tactic: convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
-- 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
h :
  ∀ (x : ℕ),
    Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
      (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)
⊢ HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
have h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)
Tactic: convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
-- 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
h :
  ∀ (x : ℕ),
    Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
      (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)
h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)
⊢ HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
have convert_1 : ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun (x : ℕ) ↦ ∅) i)
Tactic: convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
-- 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 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
h :
  ∀ (x : ℕ),
    Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
      (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)
h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)
convert_1 : ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun (x : ℕ) ↦ ∅) i)
⊢ HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
have convert_2 : Pairwise (Disjoint on Function.extend e f fun (x : ℕ) ↦ ∅)
Tactic: convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ (↑v : Set α → M) (A ∪ B) = (↑v : Set α → M) A + (↑v : Set α → M) B
have hm : ∀ (i : Bool), MeasurableSet (bif i then A else B)
Tactic: rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
hm : ∀ (i : Bool), MeasurableSet (bif i then A else B)
⊢ (↑v : Set α → M) (A ∪ B) = (↑v : Set α → M) A + (↑v : Set α → M) B
have hd : Pairwise (α := Bool) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (b : Bool) ↦ bif b then A else B)
Tactic: rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B
have rw : (↑v : Set α → M) (A ∪ B \ A) = (↑v : Set α → M) B
Tactic: rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
rw : (↑v : Set α → M) (A ∪ B \ A) = (↑v : Set α → M) B
⊢ (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B
have rw₁ : (↑v : Set α → M) B = (↑v : Set α → M) B
Tactic: rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B - (↑v : Set α → M) A
have rw : (↑v : Set α → M) (B \ A) = (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) - (↑v : Set α → M) A
Tactic: rw [← of_add_of_diff hA hB h, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
rw : (↑v : Set α → M) (B \ A) = (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) - (↑v : Set α → M) A
⊢ (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B - (↑v : Set α → M) A
have rw₁ : (↑v : Set α → M) (B \ A) = (↑v : Set α → M) (B \ A)
Tactic: rw [← of_add_of_diff hA hB h, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B = (↑v : Set α → M) A
have symm : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
have h : Disjoint (A \ B) (A ∩ B)
Tactic: rw [of_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A \ B) (A ∩ B)
⊢ (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
have hA₁ : MeasurableSet (A \ B)
Tactic: rw [of_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A \ B) (A ∩ B)
hA₁ : MeasurableSet (A \ B)
⊢ (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
have hB₁ : MeasurableSet (A ∩ B)
Tactic: rw [of_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)
have h : Disjoint (A ∩ B) (A \ B)
Tactic: rw [disjoint_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
have h : Disjoint (A ∩ B) (B \ A)
Tactic: rw [of_union, h', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A ∩ B) (B \ A)
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
have hA₁ : MeasurableSet (A ∩ B)
Tactic: rw [of_union, h', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A ∩ B) (B \ A)
hA₁ : MeasurableSet (A ∩ B)
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
have hB₁ : MeasurableSet (B \ A)
Tactic: rw [of_union, h', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have rw : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
Tactic: rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
rw : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have rw₁ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ B ∩ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
Tactic: rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
rw : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
rw₁ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ B ∩ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have rw₂ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
Tactic: rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have v₁ : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)
Tactic: calc
    v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
    _ = v (A \ B) + v (A ∩ B) := by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB
    _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
      rw [of_union, h', add_zero]
      · exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right
      · exact hA.inter hB
      · exact hB.diff hA
    _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
v₁ : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have v₂ : (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
Tactic: calc
    v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
    _ = v (A \ B) + v (A ∩ B) := by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB
    _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
      rw [of_union, h', add_zero]
      · exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right
      · exact hA.inter hB
      · exact hB.diff hA
    _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
v₁ : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)
v₂ : (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have v₃ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
Tactic: calc
    v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
    _ = v (A \ B) + v (A ∩ B) := by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB
    _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
      rw [of_union, h', add_zero]
      · exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right
      · exact hA.inter hB
      · exact hB.diff hA
    _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
v₁ : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)
v₂ : (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
v₃ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
have v₄ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
Tactic: calc
    v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
    _ = v (A \ B) + v (A ∩ B) := by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB
    _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
      rw [of_union, h', add_zero]
      · exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right
      · exact hA.inter hB
      · exact hB.diff hA
    _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ (↑s : Set α → ℝ) A
hB₂ : 0 ≤ (↑s : Set α → ℝ) B
hAB : (↑s : Set α → ℝ) (A ∪ B) = 0
⊢ (↑s : Set α → ℝ) A = 0
have hAB₁ : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
Tactic: rw [of_union h hA₁ hB₁] at hAB
Cleared hypotheses: hAB