case pos
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n

case neg
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
by_cases hf0 : f = 0
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n

case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n

case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
case neg
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
rcases lt_trichotomy (n : WithBot ℕ) (degree f) with (h | h | h)
no goals
case pos
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
simp [hf0]
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ ¬n = natDegree f
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
erw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg,
  MulZeroClass.mul_zero]
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hf0 : ¬f = 0
h : ↑(natDegree f) < degree f
⊢ False
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ ¬n = natDegree f
rintro rfl
no goals
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hf0 : ¬f = 0
h : ↑(natDegree f) < degree f
⊢ False
exact not_lt_of_ge degree_le_natDegree h
case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
this : natDegree f = n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
have : natDegree f = n := natDegree_eq_of_degree_eq_some h.symm
no goals
case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
this : natDegree f = n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
rw [coeff_C_mul, coeff_X_pow, if_pos this.symm, mul_one, leadingCoeff, this, coeff_map]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) < ↑n

case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (map (mk P) f) < ↑n
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ ↑(natDegree f) < ↑n
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) < ↑n
refine' lt_of_le_of_lt (degree_C_mul_X_pow_le _ _) _
no goals
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ ↑(natDegree f) < ↑n
rwa [← degree_eq_natDegree hf0]
no goals
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (map (mk P) f) < ↑n
exact lt_of_le_of_lt (degree_map_le _ _) h