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

case mpr
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → norm z = 0
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ norm z = 0 ↔ z = 0
constructor
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z = 0
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ norm z = 0 → z = 0
intro h
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z.re = 0 ∧ z.im = 0
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z = 0
rw [ext, zero_re, zero_im]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z.re = 0 ∧ z.im = 0
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z.re = 0 ∧ z.im = 0
rw [norm_def, sub_eq_add_neg, mul_assoc] at h
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z.re = 0 ∧ z.im = 0
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z.re = 0 ∧ z.im = 0
have left := mul_self_nonneg z.re
case mp
d✝ 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.re = 0 ∧ z.im = 0
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z.re = 0 ∧ z.im = 0
have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
case mp.intro
d✝ 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 = 0 ∧ z.im = 0
case mp
d✝ 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.re = 0 ∧ z.im = 0
obtain ⟨ha, hb⟩ := (add_eq_zero_iff' left right).mp h
case mp.intro.left.h
d✝ 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.right.h
d✝ 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
case mp.intro
d✝ 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 = 0 ∧ z.im = 0
constructor <;> apply eq_zero_of_mul_self_eq_zero
no goals
case mp.intro.left.h
d✝ 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
exact ha
case mp.intro.right.h
d✝ 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
case mp.intro.right.h
d✝ 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
rw [neg_eq_zero, mul_eq_zero] at hb
no goals
case mp.intro.right.h
d✝ 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
exact hb.resolve_left hd.ne
case mpr
d✝ d : ℤ
hd : d < 0
⊢ norm 0 = 0
case mpr
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → norm z = 0
rintro rfl
no goals
case mpr
d✝ d : ℤ
hd : d < 0
⊢ norm 0 = 0
exact norm_zero