case mp
x y : EReal
⊢ EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y → x = y

case mpr
x y : EReal
⊢ x = y → EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y
x y : EReal
⊢ EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y ↔ x = y
constructor
case mp.intro
x y : EReal
habs : EReal.abs x = EReal.abs y
hsign : ↑sign x = ↑sign y
⊢ x = y
case mp
x y : EReal
⊢ EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y → x = y
rintro ⟨habs, hsign⟩
no goals
case mp.intro
x y : EReal
habs : EReal.abs x = EReal.abs y
hsign : ↑sign x = ↑sign y
⊢ x = y
rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
case mpr
x : EReal
⊢ EReal.abs x = EReal.abs x ∧ ↑sign x = ↑sign x
case mpr
x y : EReal
⊢ x = y → EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y
rintro rfl
no goals
case mpr
x : EReal
⊢ EReal.abs x = EReal.abs x ∧ ↑sign x = ↑sign x
exact ⟨rfl, rfl⟩