-- Mathlib/NumberTheory/Multiplicity.lean
theorem sq_dvd_add_pow_sub_sub (p x : R) (n : ℕ) :
    p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * n - x ^ n

Proof state:
case succ.h
R : Type u_1
inst✝ : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ 2 ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y)

Tactic:
calc
  p ^ 2 ∣ p ^ (n + 1 - y) :=
    pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy]))
  _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) :=
    dvd_mul_of_dvd_left (dvd_mul_left _ _) _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ y + 2 ≤ n + 1

Tactic:
linarith [Finset.mem_range.mp hy]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
p x : R
⊢ p ^ 2 ∣ (x + p) ^ 0 - x ^ (0 - 1) * p * ↑0 - x ^ 0

Tactic:
simp only [pow_zero, Nat.cast_zero, sub_zero, sub_self, dvd_zero, mul_zero]

Result:
no goals

Proof state:
case succ.h
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ ∀ i ∈ range n, p ^ 2 ∣ x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Tactic:
intro y hy

Result:
case succ.h
R : Type u_1
inst✝ : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ 2 ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y)

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Tactic:
apply Finset.dvd_sum

Result:
case succ.h
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ ∀ i ∈ range n, p ^ 2 ∣ x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)

Tactic:
suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
  convert this; abel

Result:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Proof state:
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
⊢ p ^ 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)

Tactic:
convert this

Result:
case h.e'_4
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
⊢ ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1) =
    ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Proof state:
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n

Tactic:
rcases n with - | n

Result:
case zero
R : Type u_1
inst✝ : CommRing R
p x : R
⊢ p ^ 2 ∣ (x + p) ^ 0 - x ^ (0 - 1) * p * ↑0 - x ^ 0

case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * ↑(n + 1) - x ^ (n + 1)

Proof state:
case h.e'_4
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
⊢ ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1) =
    ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Tactic:
abel

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * ↑(n + 1) - x ^ (n + 1)

Tactic:
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.cast_succ, add_pow, Finset.sum_range_succ,
  Nat.choose_self, Nat.succ_sub _, tsub_self, pow_one, Nat.choose_succ_self_right, pow_zero,
  mul_one, Nat.cast_zero, zero_add, Nat.succ_eq_add_one, add_tsub_cancel_left]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)