K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
⊢ ↑(x ^ φ n) = ↑1
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
⊢ x ^ φ n ≡ 1 [MOD n]
rw [← ZMod.eq_iff_modEq_nat]
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ ↑(x ^ φ n) = ↑1
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
⊢ ↑(x ^ φ n) = ↑1
let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ ↑(x ^ φ n) = ↑1
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ ↑(x ^ φ n) = ↑1
have := ZMod.pow_totient x'
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : ↑(x' ^ φ n) = ↑1
⊢ ↑(x ^ φ n) = ↑1
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ ↑(x ^ φ n) = ↑1
apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n)  at this
no goals
K : Type ?u.971204
R : Type ?u.971207
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : ↑(x' ^ φ n) = ↑1
⊢ ↑(x ^ φ n) = ↑1
simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one,
  coe_unitOfCoprime, Units.val_pow_eq_pow_val]