d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
d a b : ℤ
⊢ ↑a ∣ ↑b ↔ a ∣ b
rw [coe_int_dvd_iff]
case mp
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im → a ∣ b

case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ (↑b).re ∧ a ∣ (↑b).im
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
constructor
case mp.intro
d a b : ℤ
hre : a ∣ (↑b).re
⊢ a ∣ b
case mp
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im → a ∣ b
rintro ⟨hre, -⟩
no goals
case mp.intro
d a b : ℤ
hre : a ∣ (↑b).re
⊢ a ∣ b
rwa [coe_int_re] at hre
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ b ∧ a ∣ 0
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ (↑b).re ∧ a ∣ (↑b).im
rw [coe_int_re, coe_int_im]
no goals
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ b ∧ a ∣ 0
exact fun hc => ⟨hc, dvd_zero a⟩