α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
rw [restrict_le_restrict_iff] at hsu hsv
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
have a := hsu (hu.diff hv) (u.diff_subset v)
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
b : ↑0 (v \ u) ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
have b := hsv (hv.diff hu) (v.diff_subset u)
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
b : ↑0 (v \ u) ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
b : ↑0 (v \ u) ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
erw [of_union (Set.disjoint_of_subset_left (u.diff_subset v) disjoint_sdiff_self_right)
    (hu.diff hv) (hv.diff hu)] at hs
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : ↑0 (u \ v) ≤ ↑s (u \ v)
b : ↑0 (v \ u) ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
rw [zero_apply] at a b
case left
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0

case right
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
constructor
no goals
case left
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0

case right
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (v \ u) = 0

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
all_goals first | linarith | infer_instance | assumption
no goals
case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
first | linarith | infer_instance | assumption
no goals
case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
linarith
case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
infer_instance
no goals
case hi
α : Type u_1
β : Type ?u.53280
inst✝² : MeasurableSpace α
s : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u
hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u
assumption