case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x * ↑abs y) * (↑(Angle.cos (↑(arg x) + ↑(arg y))) + ↑(Angle.sin (↑(arg x) + ↑(arg y))) * I)
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(arg (x * y)) = ↑(arg x) + ↑(arg y)
convert arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (abs.pos hx) (abs.pos hy))
    (arg x + arg y : Real.Angle) using
  3
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x) * ↑(↑abs y) * (exp (↑(arg x) * I) * exp (↑(arg y) * I))
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x * ↑abs y) * (↑(Angle.cos (↑(arg x) + ↑(arg y))) + ↑(Angle.sin (↑(arg x) + ↑(arg y))) * I)
simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin,
  cos_add_sin_I, ofReal_add, add_mul, exp_add, ofReal_mul]
no goals
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x) * ↑(↑abs y) * (exp (↑(arg x) * I) * exp (↑(arg y) * I))
rw [mul_assoc, mul_comm (exp _), ← mul_assoc (abs y : ℂ), abs_mul_exp_arg_mul_I, mul_comm y, ←
  mul_assoc, abs_mul_exp_arg_mul_I]