no goals
x y : EReal
⊢ -x * y = -(x * y)
induction x, y using induction₂_neg_left with
| top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top | top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
  coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
  coe_mul_bot_of_neg (neg_neg_of_pos h)]
no goals
case zero_bot

⊢ -0 * ⊥ = -(0 * ⊥)
simp only [zero_mul, mul_zero, neg_zero]
no goals
case top_bot

⊢ -⊤ * ⊥ = -(⊤ * ⊥)
rfl
no goals
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = -(-x✝ * y✝)
rw [h, neg_neg, neg_neg]
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)
case coe_coe
x✝ y✝ : ℝ
⊢ -↑x✝ * ↑y✝ = -(↑x✝ * ↑y✝)
norm_cast
no goals
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)
exact neg_mul _ _
no goals
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
no goals
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -(↑x✝ * ⊤)
rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
coe_mul_top_of_neg (neg_neg_of_pos h)]
no goals
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
no goals
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)
rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
coe_mul_bot_of_neg (neg_neg_of_pos h)]