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

R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
trans x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k
no goals
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k)
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]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
congr 1
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ∑ x_1 in Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑(Nat.choose (p ^ n) x_1 / p * p)
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ∑ x_1 in Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑(Nat.choose (p ^ n) x_1 / p * p)
refine' Finset.sum_congr rfl fun i hi => _
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
rw [mem_Ioo] at hi
no goals
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]