simp only [Int.cast_abs, Function.comp_apply, Nat.cast_one, Int.cast_one, ← Int.abs_eq_natAbs,
  Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.coe_norm]
case a
K✝ : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝⁴ : Field K✝
inst✝³ : CharZero K✝
inst✝² : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
hp✝ : p✝ ≠ 2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ (Int.cast ∘ Nat.cast) ((Algebra.norm ℤ) (1 + p • x)).natAbs = (Int.cast ∘ Nat.cast) 1
no goals