rw [← CharP.intCast_eq_intCast (ZMod n), Int.cast_pow, Int.cast_one, ←
  coe_unitOfIsCoprime' _ h, ← Units.val_pow_eq_pow_val, Units.val_eq_one, ← ZMod.pow_totient' _]
n : ℕ+
x : ℤ
h : IsCoprime x ↑↑n
⊢ x ^ φ ↑n ≡ 1 [ZMOD ↑↑n]
no goals