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