no goals
α : Type u_1
β : Type ?u.708976
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : restrict 0 i ≤ restrict s i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑↑(toMeasureOfZeroLE s i hi₁ hi) j = ↑{ val := ↑s (i ∩ j), property := (_ : 0 ≤ ↑s (i ∩ j)) }
simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
  s.restrict_apply hi₁ hj₁, Set.inter_comm]