Theorem: gaussInt.norm_mul (LeanCourse/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean)

State before:
x y : gaussInt
⊢ norm (x * y) = norm x * norm y
Tactic:
simp [norm]
State after:
x y : gaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)

State before:
x y : gaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)
Tactic:
ring
State after:
no goals