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

State before:
x : gaussInt
⊢ norm x = 0 ↔ x = 0
Tactic:
rw [norm, sq_add_sq_eq_zero, gaussInt.ext_iff]
State after:
x : gaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = 0.re ∧ x.im = 0.im

State before:
x : gaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = 0.re ∧ x.im = 0.im
Tactic:
rfl
State after:
no goals