case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
⊢ p ^ 2 ∣ (x + p) ^ Nat.zero - x ^ (Nat.zero - 1) * p * ↑Nat.zero - x ^ Nat.zero

case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ Nat.succ n - x ^ (Nat.succ n - 1) * p * ↑(Nat.succ n) - x ^ Nat.succ n
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n
cases' n with n n
no goals
case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
⊢ p ^ 2 ∣ (x + p) ^ Nat.zero - x ^ (Nat.zero - 1) * p * ↑Nat.zero - x ^ Nat.zero
simp only [pow_zero, Nat.cast_zero, sub_zero, sub_self, dvd_zero, Nat.zero_eq, mul_zero]
case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣
    ∑ m in range n, x ^ m * p ^ (n + 1 - m) * ↑(Nat.choose (n + 1) m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)
case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ Nat.succ n - x ^ (Nat.succ n - 1) * p * ↑(Nat.succ n) - x ^ Nat.succ n
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]
case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣ ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣
    ∑ m in range n, x ^ m * p ^ (n + 1 - m) * ↑(Nat.choose (n + 1) m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)
suffices p ^ 2 ∣ ∑ i : ℕ in range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
  convert this; abel
case h.e'_4
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
⊢ ∑ m in range n, x ^ m * p ^ (n + 1 - m) * ↑(Nat.choose (n + 1) m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1) =
    ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
⊢ p ^ 2 ∣
    ∑ m in range n, x ^ m * p ^ (n + 1 - m) * ↑(Nat.choose (n + 1) m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)
convert this
no goals
case h.e'_4
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
⊢ ∑ m in range n, x ^ m * p ^ (n + 1 - m) * ↑(Nat.choose (n + 1) m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1) =
    ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
abel
case succ.h
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ ∀ (x_1 : ℕ), x_1 ∈ range n → p ^ 2 ∣ x ^ x_1 * p ^ (n + 1 - x_1) * ↑(Nat.choose (n + 1) x_1)
case succ
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ p ^ 2 ∣ ∑ i in range n, x ^ i * p ^ (n + 1 - i) * ↑(Nat.choose (n + 1) i)
apply Finset.dvd_sum
case succ.h
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ 2 ∣ x ^ y * p ^ (n + 1 - y) * ↑(Nat.choose (n + 1) y)
case succ.h
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y p x : R
n : ℕ
⊢ ∀ (x_1 : ℕ), x_1 ∈ range n → p ^ 2 ∣ x ^ x_1 * p ^ (n + 1 - x_1) * ↑(Nat.choose (n + 1) x_1)
intro y hy
no goals
case succ.h
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ 2 ∣ x ^ y * p ^ (n + 1 - y) * ↑(Nat.choose (n + 1) y)
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 _ _) _
no goals
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ p x : R
n y : ℕ
hy : y ∈ range n
⊢ y + 2 ≤ n + 1
linarith [Finset.mem_range.mp hy]