no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ coeff f d = 0
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff]
case zero
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
hd✝ : ∀ (d : ℕ), d < n → coeff f d = 0
hd : ∀ (d : ℕ), d < Nat.zero → coeff f d = 0
⊢ X ^ Nat.zero ∣ f

case succ
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
⊢ X ^ Nat.succ n ∣ f
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
hd : ∀ (d : ℕ), d < n → coeff f d = 0
⊢ X ^ n ∣ f
induction' n with n hn
no goals
case zero
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
hd✝ : ∀ (d : ℕ), d < n → coeff f d = 0
hd : ∀ (d : ℕ), d < Nat.zero → coeff f d = 0
⊢ X ^ Nat.zero ∣ f
simp [pow_zero, one_dvd]
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ Nat.succ n ∣ f
case succ
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
⊢ X ^ Nat.succ n ∣ f
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : coeff (X ^ n * g) (0 + n) = coeff g 0
⊢ X ^ Nat.succ n ∣ f
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ Nat.succ n ∣ f
have := coeff_X_pow_mul g n 0
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
⊢ X ^ Nat.succ n ∣ f
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : coeff (X ^ n * g) (0 + n) = coeff g 0
⊢ X ^ Nat.succ n ∣ f
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
case succ.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ X ^ Nat.succ n ∣ f
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
⊢ X ^ Nat.succ n ∣ f
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
case succ.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ Nat.succ n * k
case succ.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ X ^ Nat.succ n ∣ f
use k
no goals
case succ.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ Nat.succ n * k
rwa [pow_succ, mul_comm X _, mul_assoc, ← hgk]