-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_zero {d : ℤ} (h_nonsquare : ∀ n : ℤ, d ≠ n * n) (a : ℤ√d) : norm a = 0 ↔ a = 0

Proof state:
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

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

Result:
no goals

Proof state:
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

Tactic:
rw [ha, mul_assoc]

Result:
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

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
suffices a.re * a.re = 0 by
  rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
  simpa only [true_and, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul,
    mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha

Result:
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

Proof state:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
by_cases h : 0 ≤ d

Result:
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 = re 0 ∧ a.im = im 0

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 = re 0 ∧ a.im = im 0

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
push_neg at h

Result:
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 = re 0 ∧ a.im = im 0

Proof state:
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

Tactic:
apply _root_.le_antisymm _ (mul_self_nonneg _)

Result:
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

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
exact divides_sq_eq_zero_z ha

Result:
no goals

Proof state:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ a.norm = 0

Tactic:
rw [h, norm_zero]

Result:
no goals

Proof state:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
⊢ a.norm = 0 ↔ a = 0

Tactic:
refine ⟨fun ha => Zsqrtd.ext_iff.mpr ?_, fun h => by rw [h, norm_zero]⟩

Result:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.norm = 0
⊢ a.re = re 0 ∧ a.im = im 0

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h

Result:
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 = re 0 ∧ a.im = im 0

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩

Result:
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 = re 0 ∧ a.im = im 0

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢

Result:
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 = re 0 ∧ a.im = im 0

Proof state:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.norm = 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
dsimp only [norm] at ha

Result:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = re 0 ∧ a.im = im 0

Proof state:
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 = re 0 ∧ a.im = im 0

Tactic:
simpa only [true_and, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul,
  mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha

Result:
no goals

Proof state:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
rw [sub_eq_zero] at ha

Result:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = re 0 ∧ a.im = im 0