case h
α : Type u_1
β : Type ?u.717548
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : restrict s Set.univ ≤ restrict 0 Set.univ
i : Set α
⊢ MeasurableSet i →
    ↑(Measure.toSignedMeasure (toMeasureOfLEZero s Set.univ (_ : MeasurableSet Set.univ) hs)) i = ↑(-s) i
α : Type u_1
β : Type ?u.717548
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hs : restrict s Set.univ ≤ restrict 0 Set.univ
⊢ Measure.toSignedMeasure (toMeasureOfLEZero s Set.univ (_ : MeasurableSet Set.univ) hs) = -s
ext i
case h
α : Type u_1
β : Type ?u.717548
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : restrict s Set.univ ≤ restrict 0 Set.univ
i : Set α
hi : MeasurableSet i
⊢ ↑(Measure.toSignedMeasure (toMeasureOfLEZero s Set.univ (_ : MeasurableSet Set.univ) hs)) i = ↑(-s) i
case h
α : Type u_1
β : Type ?u.717548
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : restrict s Set.univ ≤ restrict 0 Set.univ
i : Set α
⊢ MeasurableSet i →
    ↑(Measure.toSignedMeasure (toMeasureOfLEZero s Set.univ (_ : MeasurableSet Set.univ) hs)) i = ↑(-s) i
intro hi
no goals
case h
α : Type u_1
β : Type ?u.717548
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : restrict s Set.univ ≤ restrict 0 Set.univ
i : Set α
hi : MeasurableSet i
⊢ ↑(Measure.toSignedMeasure (toMeasureOfLEZero s Set.univ (_ : MeasurableSet Set.univ) hs)) i = ↑(-s) i
simp [hi, toMeasureOfLEZero_apply _ _ _ hi]