cases' Nat.totient_eq_one_iff.1 (show a.totient = 1 by linarith [Nat.totient_pos.2 han]) with h
    h <;>
  simp [h]
p : ℕ+
K : Type ?u.47922
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
a : ℕ
han : 0 < a
ha : a.totient ≤ 1
⊢ a ∣ 2
no goals