case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
x y : EReal
⊢ x * y = y * x
induction' x using EReal.rec with x <;> induction' y using EReal.rec with y <;>
  try { rfl }
no goals
case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
rw [← coe_mul, ← coe_mul, mul_comm]