d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ↑a * b = ↑a * c
⊢ b = c
rw [ext] at h⊢
no goals
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im
apply And.imp _ _ h <;> simpa only [smul_re, smul_im] using mul_left_cancel₀ ha