-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_leadingCoeffNth (n : ℕ) (x) :
    x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, degree p ≤ n ∧ p.leadingCoeff = x

Proof state:
case mp.intro.intro.intro.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩

Result:
case mp.intro.intro.intro.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ p.leadingCoeff = p.coeff n

Proof state:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_degree_lt hpdeg

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ ↑p.natDegree + ↑(n - p.natDegree) ≤ ↑n

Tactic:
rw [← Nat.cast_add, this]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ p.degree + (X ^ (n - p.natDegree)).degree ≤ ↑n

Tactic:
apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ ↑p.natDegree + ↑(n - p.natDegree) ≤ ↑n

Proof state:
case mp.intro.intro.intro.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ p.leadingCoeff = p.coeff n

Tactic:
rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Tactic:
rintro ⟨p, hpI, hpdeg, rfl⟩

Result:
case mpr.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
⊢ ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff

Proof state:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ Polynomial.leadingCoeff 0 = p.coeff n

Tactic:
rw [leadingCoeff_zero, eq_comm]

Result:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ p.coeff n = 0

Proof state:
case mpr.intro.intro.intro.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).degree ≤ ↑n

Tactic:
apply le_trans (degree_mul_le _ _) _

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ p.degree + (X ^ (n - p.natDegree)).degree ≤ ↑n

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) → ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Tactic:
rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩

Result:
case mp.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Proof state:
case mpr.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff

Tactic:
refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩

Result:
case mpr.intro.intro.intro.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).degree ≤ ↑n

case mpr.intro.intro.intro.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = p.leadingCoeff

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Tactic:
simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
  mem_degreeLE]

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Proof state:
case mp.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg

Result:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

case mp.intro.intro.intro.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) → ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Proof state:
case mpr.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
⊢ ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff

Tactic:
have : natDegree p + (n - natDegree p) = n :=
  add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)

Result:
case mpr.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff

Proof state:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨0, I.zero_mem, bot_le, ?_⟩

Result:
case mp.intro.intro.intro.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ Polynomial.leadingCoeff 0 = p.coeff n

Proof state:
case mpr.intro.intro.intro.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Result:
no goals