[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
⊢ ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑(p ^ (Nat.zero + 1)) ∣ a ^ p ^ Nat.zero - b ^ p ^ Nat.zero
[PROOFSTEP]
rwa [pow_one, pow_zero, pow_one, pow_one]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑(p ^ (Nat.succ k + 1)) ∣ a ^ p ^ Nat.succ k - b ^ p ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ' p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ, Nat.cast_mul]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑p * ↑(p ^ (k + 1)) ∣
    (Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
[PROOFSTEP]
refine' mul_dvd_mul _ ih
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
r : R
⊢ ↑p ∣ r ↔ ↑f r = 0
[PROOFSTEP]
rw [eq_zero_iff_mem, mem_span_singleton]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
rw [hf, map_sub, sub_eq_zero] at h 
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : ↑f a = ↑f b
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
[GOAL]
case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : ↑f a = ↑f b
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p = 0
[PROOFSTEP]
rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
