-- Mathlib/Algebra/Polynomial/Expand.lean
theorem coeff_expand {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff n = if p ∣ n then f.coeff (n / p) else 0

Proof state:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
intro hn

Result:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp only [expand_eq_sum]

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a => C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0

Tactic:
rw [if_neg]

Result:
case neg.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ ¬p * k = n

Proof state:
case neg.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ ¬p * k = n

Tactic:
exact fun hkn => h ⟨k, hkn.symm⟩

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = 0

Tactic:
rw [Finset.sum_eq_zero]

Result:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a => C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]

Result:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0

Proof state:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

Tactic:
intro b _ hb2

Result:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ (if p * b = n then f.coeff b else 0) = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = 0

Proof state:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ False

Tactic:
apply hb2

Result:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ b = n / p

Proof state:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then 0 else 0) = 0

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ ¬p * b = n

Tactic:
intro hb3

Result:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ False

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0

Tactic:
intro k _

Result:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0

Proof state:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ (if p * b = n then f.coeff b else 0) = 0

Tactic:
rw [if_neg]

Result:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ ¬p * b = n

Proof state:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ b = n / p

Tactic:
rw [← hb3, Nat.mul_div_cancel_left b hp]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)

Tactic:
rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]

Result:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Proof state:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
rw [not_mem_support_iff.1 hn]

Result:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then 0 else 0) = 0