case h
α : Type u_1
β : Type ?u.137383
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
⊢ MeasurableSet i → ↑(toSignedMeasure (μ + ν)) i = ↑(toSignedMeasure μ + toSignedMeasure ν) i
α : Type u_1
β : Type ?u.137383
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ toSignedMeasure (μ + ν) = toSignedMeasure μ + toSignedMeasure ν
ext i
case h
α : Type u_1
β : Type ?u.137383
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (μ + ν)) i = ↑(toSignedMeasure μ + toSignedMeasure ν) i
case h
α : Type u_1
β : Type ?u.137383
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
⊢ MeasurableSet i → ↑(toSignedMeasure (μ + ν)) i = ↑(toSignedMeasure μ + toSignedMeasure ν) i
intro hi
no goals
case h
α : Type u_1
β : Type ?u.137383
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (μ + ν)) i = ↑(toSignedMeasure μ + toSignedMeasure ν) i
rw [toSignedMeasure_apply_measurable hi, add_apply,
  ENNReal.toReal_add (ne_of_lt (measure_lt_top _ _)) (ne_of_lt (measure_lt_top _ _)),
  VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
  toSignedMeasure_apply_measurable hi]