no goals
x y : EReal
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, sign_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
no goals
case top_zero

⊢ ↑sign (⊤ * 0) = ↑sign ⊤ * ↑sign 0
simp only [zero_mul, mul_zero, sign_zero]
no goals
case top_top

⊢ ↑sign (⊤ * ⊤) = ↑sign ⊤ * ↑sign ⊤
rfl
no goals
case symm
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (y✝ * x✝) = ↑sign y✝ * ↑sign x✝
rwa [mul_comm, EReal.mul_comm]
no goals
case coe_coe
x✝ y✝ : ℝ
⊢ ↑sign (↑x✝ * ↑y✝) = ↑sign ↑x✝ * ↑sign ↑y✝
simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
no goals
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ↑sign (⊤ * ↑x✝) = ↑sign ⊤ * ↑sign ↑x✝
rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
no goals
case neg_left
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (-x✝ * y✝) = ↑sign (-x✝) * ↑sign y✝
rw [neg_mul, sign_neg, sign_neg, h, neg_mul]