-- Mathlib/Algebra/CharP/Lemmas.lean
theorem add_pow_prime_pow_eq (h : Commute x y) (n : ℕ) :
    (x + y) ^ p ^ n =
      x ^ p ^ n + y ^ p ^ n +
        p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i) = x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i / p * p)

Tactic:
rw [mem_Ioo] at hi

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i) = x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i / p * p)

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i) = x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i / p * p)

Tactic:
rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
simp_rw [h.add_pow, ← Nat.Ico_zero_eq_range, Nat.Ico_succ_right, Icc_eq_cons_Ico (zero_le _),
  Finset.sum_cons, Ico_eq_cons_Ioo (pow_pos hp.pos _), Finset.sum_cons, tsub_self, tsub_zero,
  pow_zero, Nat.choose_zero_right, Nat.choose_self, Nat.cast_one, mul_one, one_mul, ← add_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Tactic:
trans x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k

Result:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1 / p * p)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i) = x ^ i * y ^ (p ^ n - i) * ↑((p ^ n).choose i / p * p)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Tactic:
congr 1

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Tactic:
simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1 / p * p)