Theorem: totient_le_one_dvd_two (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
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
Tactic:
cases' Nat.totient_eq_one_iff.1 (show a.totient = 1 by linarith [Nat.totient_pos.2 han]) with h
    h <;>
  simp [h]
State after:
no goals

State before:
p : ℕ+
K : Type ?u.47922
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
a : ℕ
han : 0 < a
ha : a.totient ≤ 1
⊢ a.totient = 1
Tactic:
linarith [Nat.totient_pos.2 han]
State after:
no goals