-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_diff_of_diff_eq_zero {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B)
    (h' : v (B \ A) = 0) : v (A \ B) + v B = v A

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A) = ↑v (A \ B) + ↑v B

Tactic:
rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A)

Tactic:
rw [of_union, h', add_zero]

Result:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)

case hA
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

case hB
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (B \ A)

Proof state:
case hA
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A \ B)

Tactic:
exact hA.diff hB

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v B = ↑v A

Tactic:
symm

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B) + ↑v B

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B ∪ A ∩ B)

Tactic:
simp only [Set.diff_union_inter]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)

Tactic:
exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right

Result:
no goals

Proof state:
case hA
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

Tactic:
exact hA.inter hB

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B ∪ A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B)

Tactic:
rw [of_union]

Result:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)

case hA
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A \ B)

case hB
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

Proof state:
case hB
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (B \ A)

Tactic:
exact hB.diff hA

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)

Tactic:
rw [disjoint_comm]

Result:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)

Proof state:
case hB
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

Tactic:
exact hA.inter hB

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)

Tactic:
exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right

Result:
no goals