α : Type u_1
β : Type ?u.712523
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict s i ≤ restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑{ val := ↑(-s) (i ∩ j), property := (_ : 0 ≤ ↑(-s) (i ∩ j)) } =
    ↑{ val := -↑s (i ∩ j), property := (_ : 0 ≤ -↑s (i ∩ j)) }

case hj₁
α : Type u_1
β : Type ?u.712523
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict s i ≤ restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ MeasurableSet j
α : Type u_1
β : Type ?u.712523
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict s i ≤ restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑↑(toMeasureOfLEZero s i hi₁ hi) j = ↑{ val := -↑s (i ∩ j), property := (_ : 0 ≤ -↑s (i ∩ j)) }
erw [toMeasureOfZeroLE_apply]
no goals
α : Type u_1
β : Type ?u.712523
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict s i ≤ restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑{ val := ↑(-s) (i ∩ j), property := (_ : 0 ≤ ↑(-s) (i ∩ j)) } =
    ↑{ val := -↑s (i ∩ j), property := (_ : 0 ≤ -↑s (i ∩ j)) }
simp
no goals
case hj₁
α : Type u_1
β : Type ?u.712523
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict s i ≤ restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ MeasurableSet j
assumption