-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_pow_modEq_one (p m a : ℕ) : (1 + p * a) ^ (p ^ m) ≡ 1 [MOD p ^ m]

Proof state:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
k : ℕ
hk : k ∈ range p
⊢ p ∣ (p ^ m * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases m

Result:
case succ.intro.zero
p a d k : ℕ
hk : k ∈ range p
hd : (1 + p * a) ^ p ^ 0 = p ^ 0 * d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

case succ.intro.succ
p a d k : ℕ
hk : k ∈ range p
n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ k * ↑(p.choose (k + 1))

Proof state:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1))

Tactic:
simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]

Result:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * ↑(p.choose (i + 1)))

Proof state:
p m a : ℕ
⊢ (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]

Tactic:
induction' m with m hm

Result:
case zero
p a : ℕ
⊢ (1 + p * a) ^ p ^ 0 ≡ 1 [MOD p ^ 0]

case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Proof state:
case succ.intro.succ
p a d k : ℕ
hk : k ∈ range p
n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k <;> simp [mul_assoc, pow_succ']

Result:
no goals

Proof state:
case zero
p a : ℕ
⊢ (1 + p * a) ^ p ^ 0 ≡ 1 [MOD p ^ 0]

Tactic:
exact Nat.modEq_one

Result:
no goals

Proof state:
case succ.intro.zero
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k <;> simp [← hd, mul_assoc, pow_succ']

Result:
no goals

Proof state:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + 1 ≡ 1 [MOD p ^ m * p]

Tactic:
refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)

Result:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1))

Proof state:
case succ
p a m : ℕ
hm : p ^ m ∣ (p * a + 1) ^ p ^ m - 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
obtain ⟨d, hd⟩ := hm

Result:
case succ.intro
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Proof state:
case succ.intro
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd

Result:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Proof state:
case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm

Result:
case succ
p a m : ℕ
hm : p ^ m ∣ (p * a + 1) ^ p ^ m - 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Proof state:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow,
  one_mul, Nat.choose_zero_right, Nat.cast_one]

Result:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + 1 ≡ 1 [MOD p ^ m * p]

Proof state:
case succ.intro.zero
p a d k : ℕ
hk : k ∈ range p
hd : (1 + p * a) ^ p ^ 0 = p ^ 0 * d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd

Result:
case succ.intro.zero
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Proof state:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * ↑(p.choose (i + 1)))

Tactic:
refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)

Result:
case succ.intro
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
k : ℕ
hk : k ∈ range p
⊢ p ∣ (p ^ m * d) ^ k * ↑(p.choose (k + 1))