multiplication of complex number

Stream: new members

[Artizuiala G.]

I'm trying to prove the multiplication law of complex number before I use it to proving other things.
for example, I have two complex number, x = a + bi, y = c + di, and w.t.s x * y = (ac - bd) + i (ad + bc).
sor far, I tried:

example : ∀ (x y : ℂ), (∃ (a b : ℤ), x = a + complex.I * b) → (∃ (c d : ℤ), y = c + complex.I * d) → (∃ (e f : ℤ), x * y = e + complex.I * f) :=
begin
  intros x y,
  intros hx hy,
  obtain ⟨a, b, hx⟩ := hx,
  obtain ⟨c, d, hy⟩ := hy,
  -- w.t.s x * y = (a * c - b * d) + complex.I * (a * d + b * c)
  use a * c - b * d, -- x = ↑a + complex.I * ↑b
  use a * d + b * c, -- y = ↑c + complex.I * ↑d
  have hxy : x * y = (↑a + complex.I * ↑b) * (↑c + complex.I * ↑d),
     exact congr (congr_arg has_mul.mul hx) hy,
  have h3 : (x * y).re = (x.re) * y.re - (x.im) * y.im,
       exact complex.mul_re x y,
  have h4 : (x * y).im = (x.re) * y.im + (x.im) * y.re,
       exact complex.mul_im x y,
  -- have h5 : x.re = a,
  sorry,
end

I have no idea how to do next, any suggestions?