-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem isCoprime_of_dvd_isCoprime {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b ∣ a) :
    IsCoprime b.re b.im

Proof state:
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re 0 = 0
him : im 0 = 0
⊢ False

Tactic:
rw [zero_dvd_iff] at hdvd

Result:
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : re 0 = 0
him : im 0 = 0
⊢ False

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

Tactic:
exact ⟨hzdvdu, hzdvdv⟩

Result:
no goals

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

Tactic:
apply hz

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

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

Tactic:
rw [intCast_dvd]

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

Proof state:
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ b.re → ¬z ∣ b.im

Tactic:
rintro z hz - hzdvdu hzdvdv

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

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

Tactic:
apply dvd_trans _ hdvd

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

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

Tactic:
rintro ⟨hre, him⟩

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

Proof state:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im

Tactic:
apply isCoprime_of_dvd

Result:
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 ∈ nonunits ℤ, z ≠ 0 → z ∣ b.re → ¬z ∣ b.im

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

Tactic:
exact hcoprime.isUnit_of_dvd' ha hb

Result:
no goals

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

Tactic:
rw [← intCast_dvd]

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

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

Tactic:
obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
  rw [← intCast_dvd]
  apply dvd_trans _ hdvd
  rw [intCast_dvd]
  exact ⟨hzdvdu, hzdvdv⟩

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

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

Tactic:
obtain rfl : b = 0 := Zsqrtd.ext hre him

Result:
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re 0 = 0
him : im 0 = 0
⊢ False

Proof state:
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : re 0 = 0
him : im 0 = 0
⊢ False

Tactic:
simp [hdvd, zero_im, zero_re, not_isCoprime_zero_zero] at hcoprime

Result:
no goals