R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
⊢ a = 0
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ ↑(↑lift r) ↑(norm a) = 0
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0
suffices lift r a.norm = 0 by
  simp only [coe_int_re, add_zero, lift_apply_apply, coe_int_im, Int.cast_zero,
    MulZeroClass.zero_mul] at this
  rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
no goals
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ ↑(↑lift r) ↑(norm a) = 0
rw [norm_eq_mul_conj, RingHom.map_mul, ha, MulZeroClass.zero_mul]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑(norm a) = 0
⊢ a = 0
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑(↑lift r) ↑(norm a) = 0
⊢ a = 0
simp only [coe_int_re, add_zero, lift_apply_apply, coe_int_im, Int.cast_zero,
  MulZeroClass.zero_mul] at this
no goals
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑(norm a) = 0
⊢ a = 0
rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this