case nonzero
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ¬(b.re = 0 ∧ b.im = 0)

case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ∀ (z : ℤ), z ∈ nonunits ℤ → z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im
apply isCoprime_of_dvd
case nonzero.intro
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ False
case nonzero
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ¬(b.re = 0 ∧ b.im = 0)
rintro ⟨hre, him⟩
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : 0.re = 0
him : 0.im = 0
⊢ False
case nonzero.intro
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ False
obtain rfl : b = 0 := by
  simp only [ext, hre, eq_self_iff_true, zero_im, him, and_self_iff, zero_re]
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : 0.re = 0
him : 0.im = 0
⊢ False
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : 0.re = 0
him : 0.im = 0
⊢ False
rw [zero_dvd_iff] at hdvd
no goals
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : 0.re = 0
him : 0.im = 0
⊢ False
simp [hdvd, zero_im, zero_re, not_isCoprime_zero_zero] at hcoprime
no goals
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ b = 0
simp only [ext, hre, eq_self_iff_true, zero_im, him, and_self_iff, zero_re]
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ False
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ∀ (z : ℤ), z ∈ nonunits ℤ → z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
rintro z hz - hzdvdu hzdvdv
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ IsUnit z
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ False
apply hz
case H.intro
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
hb : z ∣ a.im
⊢ IsUnit z
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ IsUnit z
obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
  rw [← coe_int_dvd_iff]
  apply dvd_trans _ hdvd
  rw [coe_int_dvd_iff]
  exact ⟨hzdvdu, hzdvdv⟩
no goals
case H.intro
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
hb : z ∣ a.im
⊢ IsUnit z
exact hcoprime.isUnit_of_dvd' ha hb
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ a
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ a.re ∧ z ∣ a.im
rw [← coe_int_dvd_iff]
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ b
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ a
apply dvd_trans _ hdvd
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ b
rw [coe_int_dvd_iff]
no goals
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im
exact ⟨hzdvdu, hzdvdv⟩