-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem of_inter_eq_of_symmDiff_eq_zero_positive (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hw : MeasurableSet w) (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) :
    s (w ∩ u) = s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
obtain ⟨huv, hvu⟩ :=
  of_diff_eq_zero_of_symmDiff_eq_zero_positive (hw.inter hu) (hw.inter hv)
    (restrict_le_restrict_subset _ _ hu hsu (w.inter_subset_right))
    (restrict_le_restrict_subset _ _ hv hsv (w.inter_subset_right)) hwuv

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
huv : ↑s ((w ∩ u) \ (w ∩ v)) = 0
hvu : ↑s ((w ∩ v) \ (w ∩ u)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v

Tactic:
rw [← Set.inter_symmDiff_distrib_left]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
have hwuv : s ((w ∩ u) ∆ (w ∩ v)) = 0 := by
  refine
    subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv))
      (hu.symmDiff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs
      Set.symmDiff_subset_union ?_
  rw [← Set.inter_symmDiff_distrib_left]
  exact Set.inter_subset_right

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v

Tactic:
exact Set.inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ ↑s ((w ∩ u) ∆ (w ∩ v)) = 0

Tactic:
refine
  subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv))
    (hu.symmDiff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs
    Set.symmDiff_subset_union ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
huv : ↑s ((w ∩ u) \ (w ∩ v)) = 0
hvu : ↑s ((w ∩ v) \ (w ∩ u)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)

Tactic:
rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]

Result:
no goals