d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : norm a = 0
⊢ a.re = 0.re ∧ a.im = 0.im
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
⊢ norm a = 0 ↔ a = 0
refine' ⟨fun ha => ext.mpr _, fun h => by rw [h, norm_zero]⟩
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = 0.re ∧ a.im = 0.im
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : norm a = 0
⊢ a.re = 0.re ∧ a.im = 0.im
dsimp only [norm] at ha
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = 0.re ∧ a.im = 0.im
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = 0.re ∧ a.im = 0.im
rw [sub_eq_zero] at ha
case pos
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im

case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : ¬0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = 0.re ∧ a.im = 0.im
by_cases h : 0 ≤ d
no goals
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ norm a = 0
rw [h, norm_zero]
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
⊢ a.re = 0.re ∧ a.im = 0.im
case pos
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im
obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
this : Nonsquare d'
⊢ a.re = 0.re ∧ a.im = 0.im
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
⊢ a.re = 0.re ∧ a.im = 0.im
haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| by exact_mod_cast h⟩
no goals
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
this : Nonsquare d'
⊢ a.re = 0.re ∧ a.im = 0.im
exact divides_sq_eq_zero_z ha
no goals
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h✝ : 0 ≤ ↑d'
n : ℕ
h : d' = n * n
⊢ ↑d' = ↑n * ↑n
exact_mod_cast h
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = 0.re ∧ a.im = 0.im
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : ¬0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im
push_neg at h
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re = 0
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = 0.re ∧ a.im = 0.im
suffices a.re * a.re = 0 by
  rw [eq_zero_of_mul_self_eq_zero this] at ha⊢
  simpa only [true_and_iff, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul,
    mul_zero, mul_eq_zero, h.ne, false_or_iff, or_self_iff] using ha
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re ≤ 0
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re = 0
apply _root_.le_antisymm _ (mul_self_nonneg _)
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re ≤ 0
rw [ha, mul_assoc]
no goals
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : 0 * 0 = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ 0 = 0.re ∧ a.im = 0.im
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ a.re = 0.re ∧ a.im = 0.im
rw [eq_zero_of_mul_self_eq_zero this] at ha⊢
no goals
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : 0 * 0 = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ 0 = 0.re ∧ a.im = 0.im
simpa only [true_and_iff, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul,
  mul_zero, mul_eq_zero, h.ne, false_or_iff, or_self_iff] using ha