English
For all x,y ∈ EReal, toReal (x*y) = toReal x * toReal y.
Русский
Для всех x,y ∈ EReal: toReal(x*y) = toReal x * toReal y.
LaTeX
$$$\operatorname{toReal}(x \cdot y) = \operatorname{toReal}(x) \cdot \operatorname{toReal}(y)$$$
Lean4
theorem toReal_mul {x y : EReal} : toReal (x * y) = toReal x * toReal y := by
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]
