-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem map_eq_C_mul_X_pow_of_forall_coeff_mem {f : R[X]} {P : Ideal R}
    (hfP : ∀ n : ℕ, ↑n < f.degree → f.coeff n ∈ P) :
    map (mk P) f = C ((mk P) f.leadingCoeff) * X ^ f.natDegree :=
  Polynomial.ext fun n => by
    by_cases hf0 : f = 0
    · simp [hf0]
    rcases lt_trichotomy (n : WithBot ℕ) (degree f) with (h | h | h)
    · rw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg, mul_zero]
      rintro rfl
      exact not_lt_of_ge degree_le_natDegree h
    · have : natDegree f = n := natDegree_eq_of_degree_eq_some h.symm
      rw [coeff_C_mul, coeff_X_pow, if_pos this.symm, mul_one, leadingCoeff, this, coeff_map]
    · rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt]
      · refine lt_of_le_of_lt (degree_C_mul_X_pow_le _ _) ?_
        rwa [← degree_eq_natDegree hf0]
      · exact lt_of_le_of_lt degree_map_le h

Proof state:
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < f.degree
⊢ ¬n = f.natDegree

Tactic:
rintro rfl

Result:
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hf0 : ¬f = 0
h : ↑f.natDegree < f.degree
⊢ False

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

Tactic:
rw [coeff_C_mul, coeff_X_pow, if_pos this.symm, mul_one, leadingCoeff, this, coeff_map]

Result:
no goals

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

Tactic:
rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt]

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

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

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

Tactic:
rw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg, mul_zero]

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

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

Tactic:
by_cases hf0 : f = 0

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

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

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

Tactic:
have : natDegree f = n := natDegree_eq_of_degree_eq_some h.symm

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

Proof state:
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hf0 : ¬f = 0
h : ↑f.natDegree < f.degree
⊢ False

Tactic:
exact not_lt_of_ge degree_le_natDegree h

Result:
no goals

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

Tactic:
simp [hf0]

Result:
no goals

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

Tactic:
exact lt_of_le_of_lt degree_map_le h

Result:
no goals

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

Tactic:
rwa [← degree_eq_natDegree hf0]

Result:
no goals

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

Tactic:
rcases lt_trichotomy (n : WithBot ℕ) (degree f) with (h | h | h)

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

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

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

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

Tactic:
refine lt_of_le_of_lt (degree_C_mul_X_pow_le _ _) ?_

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