case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ coeff (↑(expand R p) (contract p f)) n = coeff f n
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
⊢ ↑(expand R p) (contract p f) = f
ext n
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then coeff f (n / p * p) else 0) = coeff f n
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ coeff (↑(expand R p) (contract p f)) n = coeff f n
rw [coeff_expand hp.bot_lt, coeff_contract hp]
case a.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ coeff f (n / p * p) = coeff f n

case a.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = coeff f n
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then coeff f (n / p * p) else 0) = coeff f n
split_ifs with h
no goals
case a.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ coeff f (n / p * p) = coeff f n
rw [Nat.div_mul_cancel h]
case a.inr.zero
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
h : ¬p ∣ Nat.zero
⊢ 0 = coeff f Nat.zero

case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
case a.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = coeff f n
cases' n with n
case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff (↑derivative f) n = coeff f (n + 1) * (↑n + 1)
⊢ 0 = coeff f (Nat.succ n)
case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
have := coeff_derivative f n
case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff f (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff (↑derivative f) n = coeff f (n + 1) * (↑n + 1)
⊢ 0 = coeff f (Nat.succ n)
rw [hf, coeff_zero, zero_eq_mul] at this
case a.inr.succ.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : coeff f (n + 1) = 0
⊢ 0 = coeff f (Nat.succ n)

case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h✝ : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
case a.inr.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff f (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
cases' this with h'
case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h✝ : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
rename_i _ _ _ _ h'
case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
no goals
case a.inr.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
exact absurd h' h
no goals
case a.inr.zero
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
h : ¬p ∣ Nat.zero
⊢ 0 = coeff f Nat.zero
exact absurd (dvd_zero p) h
no goals
case a.inr.succ.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : coeff f (n + 1) = 0
⊢ 0 = coeff f (Nat.succ n)
rw [h']