no goals
⊢ ↑(↑sign ⊥) * ↑(EReal.abs ⊥) = ⊥
simp
no goals
⊢ ↑(↑sign ⊤) * ↑(EReal.abs ⊤) = ⊤
simp
no goals
x : ℝ
⊢ ↑(↑sign ↑x) * ↑(EReal.abs ↑x) = ↑x
rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]