-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_contract [CharP R p] [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0)
    (hp : p ≠ 0) : expand R p (contract p f) = f

Proof state:
case neg.zero
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
h : ¬p ∣ 0
⊢ 0 = f.coeff 0

Tactic:
exact absurd (dvd_zero p) h

Result:
no goals

Proof state:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : (derivative f).coeff n = f.coeff (n + 1) * (↑n + 1)
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [hf, coeff_zero, zero_eq_mul] at this

Result:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Proof state:
case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n

Tactic:
rw [Nat.div_mul_cancel h]

Result:
no goals

Proof state:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)

Tactic:
have := coeff_derivative f n

Result:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : (derivative f).coeff n = f.coeff (n + 1) * (↑n + 1)
⊢ 0 = f.coeff (n + 1)

Proof state:
case a
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n

case neg
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = f.coeff n

Proof state:
case neg
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = f.coeff n

Tactic:
rcases n with - | n

Result:
case neg.zero
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
h : ¬p ∣ 0
⊢ 0 = f.coeff 0

case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)

Proof state:
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
⊢ (expand R p) (contract p f) = f

Tactic:
ext n

Result:
case a
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ ((expand R p) (contract p f)).coeff n = f.coeff n

Proof state:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rcases this with h' | _

Result:
case neg.succ.inl
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)

case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h✝ : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Proof state:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'

Result:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Proof state:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Tactic:
exact absurd h' h

Result:
no goals

Proof state:
case a
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ ((expand R p) (contract p f)).coeff n = f.coeff n

Tactic:
rw [coeff_expand hp.bot_lt, coeff_contract hp]

Result:
case a
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n

Proof state:
case neg.succ.inl
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [h']

Result:
no goals

Proof state:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h✝ : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rename_i _ _ _ h'

Result:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)