case posPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁.posPart = j₂.posPart

case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁.negPart = j₂.negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁ = j₂
ext1
no goals
case posPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁.posPart = j₂.posPart
exact hj
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ j₁.negPart = j₂.negPart
rw [← toSignedMeasure_eq_toSignedMeasure_iff]
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' :
  Measure.toSignedMeasure j₁.posPart - Measure.toSignedMeasure j₁.negPart =
    Measure.toSignedMeasure j₂.posPart - Measure.toSignedMeasure j₂.negPart
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : toSignedMeasure j₁ = toSignedMeasure j₂
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
unfold toSignedMeasure at hj'
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' :
  Measure.toSignedMeasure j₁.posPart - Measure.toSignedMeasure j₁.negPart =
    Measure.toSignedMeasure j₂.posPart - Measure.toSignedMeasure j₂.negPart
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
simp_rw [hj, sub_right_inj] at hj'
no goals
case negPart
α : Type u_1
β : Type ?u.69483
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
⊢ Measure.toSignedMeasure j₁.negPart = Measure.toSignedMeasure j₂.negPart
exact hj'