Theorem: ZMod.pow_totient' (AlgebraI/Subgroups.lean)

State before:
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1
Tactic:
cases n
State after:
case zero
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1

case succ
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1

State before:
case succ
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
Tactic:
apply ZMod.pow_totient
State after:
no goals

State before:
case zero
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1
Tactic:
simp
State after:
no goals