case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
constructor
case mp.intro
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im
case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im
rintro ⟨x, rfl⟩
no goals
case mp.intro
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im
simp only [add_zero, coe_int_re, MulZeroClass.zero_mul, mul_im, dvd_mul_right, and_self_iff,
  mul_re, mul_zero, coe_int_im]
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a
case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a
rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a
use ⟨r, i⟩
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = { re := z * r, im := z * i }.re ∧ a.im = { re := z * r, im := z * i }.im
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }
rw [smul_val, ext]
no goals
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = { re := z * r, im := z * i }.re ∧ a.im = { re := z * r, im := z * i }.im
exact ⟨hr, hi⟩