case refine'_1
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
⊢ μ = ν

case refine'_2
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ toSignedMeasure μ = toSignedMeasure ν
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ toSignedMeasure μ = toSignedMeasure ν ↔ μ = ν
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.h
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ i = ↑↑ν i
case refine'_1
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
⊢ μ = ν
ext1 i hi
case refine'_1.h
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
this : ↑(toSignedMeasure μ) i = ↑(toSignedMeasure ν) i
⊢ ↑↑μ i = ↑↑ν i
case refine'_1.h
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ i = ↑↑ν i
have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]
no goals
case refine'_1.h
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
this : ↑(toSignedMeasure μ) i = ↑(toSignedMeasure ν) i
⊢ ↑↑μ i = ↑↑ν i
rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
    ENNReal.toReal_eq_toReal] at this
  <;> exact measure_ne_top _ _
no goals
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure μ) i = ↑(toSignedMeasure ν) i
rw [h]
no goals
case refine'_2
α : Type u_1
β : Type ?u.135386
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ toSignedMeasure μ = toSignedMeasure ν
congr