-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) : z.norm = 0 ↔ z = 0

Proof state:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
⊢ z = 0

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h

Result:
case mp.intro
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z = 0

Proof state:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z = 0

Tactic:
have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))

Result:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
⊢ z = 0

Proof state:
case mp.intro.im.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0

Tactic:
exact hb.resolve_left hd.ne

Result:
no goals

Proof state:
case mp.intro.re.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

Tactic:
exact ha

Result:
no goals

Proof state:
case mp.intro
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z = 0

Tactic:
ext <;> apply eq_zero_of_mul_self_eq_zero

Result:
case mp.intro.re.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

case mp.intro.im.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0

Proof state:
case mpr
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → z.norm = 0

Tactic:
rintro rfl

Result:
case mpr
d : ℤ
hd : d < 0
⊢ norm 0 = 0

Proof state:
case mp.intro.im.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0

Tactic:
rw [neg_eq_zero, mul_eq_zero] at hb

Result:
case mp.intro.im.h
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0

Proof state:
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 ↔ z = 0

Tactic:
constructor

Result:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 → z = 0

case mpr
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → z.norm = 0

Proof state:
case mpr
d : ℤ
hd : d < 0
⊢ norm 0 = 0

Tactic:
exact norm_zero

Result:
no goals

Proof state:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0

Tactic:
rw [norm_def, sub_eq_add_neg, mul_assoc] at h

Result:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z = 0

Proof state:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z = 0

Tactic:
have left := mul_self_nonneg z.re

Result:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z = 0

Proof state:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 → z = 0

Tactic:
intro h

Result:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0