no goals
x y : EReal
⊢ EReal.abs (x * y) = EReal.abs x * EReal.abs y
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, abs_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
  rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
  exact h.ne'
| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
no goals
case top_zero

⊢ EReal.abs (⊤ * 0) = EReal.abs ⊤ * EReal.abs 0
simp only [zero_mul, mul_zero, abs_zero]
no goals
case top_top

⊢ EReal.abs (⊤ * ⊤) = EReal.abs ⊤ * EReal.abs ⊤
rfl
no goals
case symm
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (y✝ * x✝) = EReal.abs y✝ * EReal.abs x✝
rwa [mul_comm, EReal.mul_comm]
no goals
case coe_coe
x✝ y✝ : ℝ
⊢ EReal.abs (↑x✝ * ↑y✝) = EReal.abs ↑x✝ * EReal.abs ↑y✝
simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs ↑x✝ ≠ 0
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs (⊤ * ↑x✝) = EReal.abs ⊤ * EReal.abs ↑x✝
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs ↑x✝ ≠ 0
rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
no goals
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0
exact h.ne'
no goals
case neg_left
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (-x✝ * y✝) = EReal.abs (-x✝) * EReal.abs y✝
rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]