-- Mathlib/Algebra/Polynomial/Div.lean
theorem X_pow_dvd_iff {f : R[X]} {n : ℕ} : X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0 :=
  ⟨fun ⟨g, hgf⟩ d hd => by
    simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff],
    fun hd => by
    induction n with
    | zero => simp [pow_zero, one_dvd]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]⟩

Proof state:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ (n + 1) ∣ f

Tactic:
have := coeff_X_pow_mul g n 0

Result:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : (X ^ n * g).coeff (0 + n) = g.coeff 0
⊢ X ^ (n + 1) ∣ f

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
⊢ X ^ n ∣ f

Tactic:
induction n with
| zero => simp [pow_zero, one_dvd]
| succ n hn =>
  obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
  have := coeff_X_pow_mul g n 0
  rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
  obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
  use k
  rwa [pow_succ, mul_assoc, ← hgk]

Result:
no goals

Proof state:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
⊢ X ^ (n + 1) ∣ f

Tactic:
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm

Result:
case succ.intro.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ X ^ (n + 1) ∣ f

Proof state:
case succ.intro.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ X ^ (n + 1) ∣ f

Tactic:
use k

Result:
case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ (n + 1) * k

Proof state:
case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
⊢ X ^ (n + 1) ∣ f

Tactic:
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)

Result:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ (n + 1) ∣ f

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ f.coeff d = 0

Tactic:
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
f : R[X]
hd : ∀ d < 0, f.coeff d = 0
⊢ X ^ 0 ∣ f

Tactic:
simp [pow_zero, one_dvd]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ (n + 1) * k

Tactic:
rwa [pow_succ, mul_assoc, ← hgk]

Result:
no goals

Proof state:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : (X ^ n * g).coeff (0 + n) = g.coeff 0
⊢ X ^ (n + 1) ∣ f

Tactic:
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this

Result:
case succ.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
⊢ X ^ (n + 1) ∣ f