α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)
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 _ _
case intro
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
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)
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
⊢ ↑s (w ∩ u) = ↑s (w ∩ v)
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 u))
    (restrict_le_restrict_subset _ _ hv hsv (w.inter_subset_right v)) hwuv
no goals
case intro
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
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)
rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ ↑s ((w ∩ u) ∆ (w ∩ v)) = 0
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 _
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v
rw [← Set.inter_symmDiff_distrib_left]
no goals
α : Type u_1
β : Type ?u.63811
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v
exact Set.inter_subset_right _ _