no goals
x y : EReal
⊢ toReal (x * y) = toReal x * toReal y
induction x, y using induction₂_symm with
| top_zero | zero_bot | top_top | top_bot | bot_bot => simp
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => norm_cast
| top_pos _ h => simp [top_mul_coe_of_pos h]
| top_neg _ h => simp [top_mul_coe_of_neg h]
| pos_bot _ h => simp [coe_mul_bot_of_pos h]
| neg_bot _ h => simp [coe_mul_bot_of_neg h]
no goals
case bot_bot

⊢ toReal (⊥ * ⊥) = toReal ⊥ * toReal ⊥
simp
no goals
case symm
x✝ y✝ : EReal
h : toReal (x✝ * y✝) = toReal x✝ * toReal y✝
⊢ toReal (y✝ * x✝) = toReal y✝ * toReal x✝
rwa [mul_comm, EReal.mul_comm]
no goals
case coe_coe
x✝ y✝ : ℝ
⊢ toReal (↑x✝ * ↑y✝) = toReal ↑x✝ * toReal ↑y✝
norm_cast
no goals
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
simp [top_mul_coe_of_pos h]
no goals
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
simp [top_mul_coe_of_neg h]
no goals
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
simp [coe_mul_bot_of_pos h]
no goals
case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
simp [coe_mul_bot_of_neg h]