Euler's theorem (modular)

import Mathlib

theorem euler_thm (n : ℕ) (a : ℤ) (h : IsCoprime a n) : a ^ Nat.totient n ≡ 1 [ZMOD n] :=by
  by_cases hn : n = 0
  · subst hn
    simp
  haveI : NeZero n := ⟨hn⟩
  rw [← ZMod.intCast_eq_intCast_iff]
  push_cast
  let u := ZMod.unitOfIsCoprime a h
  have hu : (a : ZMod n) = ↑u := (ZMod.coe_unitOfIsCoprime a h).symm
  rw [hu]
  rw [← Units.val_pow_eq_pow_val]
  rw [ZMod.pow_totient u]
  rfl