α : Type u_1
β : Type ?u.720670
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) Set.univ (_ : MeasurableSet Set.univ)
            (_ : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict (toSignedMeasure μ) Set.univ))
      i =
    ↑↑μ i
α : Type u_1
β : Type ?u.720670
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) Set.univ (_ : MeasurableSet Set.univ)
      (_ : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict (toSignedMeasure μ) Set.univ) =
    μ
refine' Measure.ext fun i hi => _
case intro
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) Set.univ (_ : MeasurableSet Set.univ)
            (_ : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict (toSignedMeasure μ) Set.univ))
      i =
    ↑m
α : Type u_1
β : Type ?u.720670
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) Set.univ (_ : MeasurableSet Set.univ)
            (_ : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict (toSignedMeasure μ) Set.univ))
      i =
    ↑↑μ i
lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
case intro
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ { val := ↑(toSignedMeasure μ) (Set.univ ∩ i), property := (_ : 0 ≤ ↑(toSignedMeasure μ) (Set.univ ∩ i)) } = m
case intro
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) Set.univ (_ : MeasurableSet Set.univ)
            (_ : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict (toSignedMeasure μ) Set.univ))
      i =
    ↑m
rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, coe_eq_coe]
case intro.e_val
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑(toSignedMeasure μ) (Set.univ ∩ i) = ↑m
case intro
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ { val := ↑(toSignedMeasure μ) (Set.univ ∩ i), property := (_ : 0 ≤ ↑(toSignedMeasure μ) (Set.univ ∩ i)) } = m
congr
no goals
case intro.e_val
α : Type u_1
β : Type ?u.720670
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑(toSignedMeasure μ) (Set.univ ∩ i) = ↑m
simp [hi, ← hm]