no goals
d : ℤ
x : ℤ√d
h : Int.natAbs (norm x) = 1
hx : 0 ≤ norm x
⊢ 1 = x * star x
rwa [← Int.coe_nat_inj', Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _,
  norm_eq_mul_conj, eq_comm] at h
no goals
d : ℤ
x : ℤ√d
h : Int.natAbs (norm x) = 1
hx : norm x ≤ 0
⊢ 1 = x * -star x
rwa [← Int.coe_nat_inj', Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
  Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ Int.natAbs (norm x) = 1
d : ℤ
x : ℤ√d
h : IsUnit x
⊢ Int.natAbs (norm x) = 1
let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ Int.natAbs (norm x) = 1
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ Int.natAbs (norm x) = 1
have := congr_arg (Int.natAbs ∘ norm) hy
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Int.natAbs (norm x) = 1 ∧ Int.natAbs (norm y) = 1
⊢ Int.natAbs (norm x) = 1
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ Int.natAbs (norm x) = 1
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
  Int.natAbs_one, eq_comm, mul_eq_one] at this
no goals
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Int.natAbs (norm x) = 1 ∧ Int.natAbs (norm y) = 1
⊢ Int.natAbs (norm x) = 1
exact this.1