R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x) ↔
    ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ x ∈ leadingCoeffNth I n ↔ ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x
simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
  mem_degreeLE]
case mp
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x) →
    ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x

case mpr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x) →
    ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x) ↔
    ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x
constructor
case mp.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n
case mp
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x) →
    ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x
rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n

case mp.intro.intro.intro.inr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p = ↑n
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n
case mp.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n
cases' lt_or_eq_of_le hpdeg with hpdeg hpdeg
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ Polynomial.leadingCoeff 0 = coeff p n
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n
refine' ⟨0, I.zero_mem, bot_le, _⟩
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ coeff p n = 0
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ Polynomial.leadingCoeff 0 = coeff p n
rw [leadingCoeff_zero, eq_comm]
no goals
case mp.intro.intro.intro.inl
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p < ↑n
⊢ coeff p n = 0
exact coeff_eq_zero_of_degree_lt hpdeg
case mp.intro.intro.intro.inr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p = ↑n
⊢ Polynomial.leadingCoeff p = coeff p n
case mp.intro.intro.intro.inr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p = ↑n
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = coeff p n
refine' ⟨p, hpI, le_of_eq hpdeg, _⟩
no goals
case mp.intro.intro.intro.inr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : degree p ≤ ↑n
hpI : p ∈ ofPolynomial I
hpdeg : degree p = ↑n
⊢ Polynomial.leadingCoeff p = coeff p n
rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbot'_coe]
case mpr.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
⊢ ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = Polynomial.leadingCoeff p
case mpr
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x) →
    ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = x
rintro ⟨p, hpI, hpdeg, rfl⟩
case mpr.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = Polynomial.leadingCoeff p
case mpr.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
⊢ ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = Polynomial.leadingCoeff p
have : natDegree p + (n - natDegree p) = n :=
  add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
case mpr.intro.intro.intro.refine'_1
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ degree (p * X ^ (n - natDegree p)) ≤ ↑n

case mpr.intro.intro.intro.refine'_2
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ coeff (p * X ^ (n - natDegree p)) n = Polynomial.leadingCoeff p
case mpr.intro.intro.intro
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ ∃ y, (degree y ≤ ↑n ∧ y ∈ ofPolynomial I) ∧ coeff y n = Polynomial.leadingCoeff p
refine' ⟨p * X ^ (n - natDegree p), ⟨_, I.mul_mem_right _ hpI⟩, _⟩
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ degree p + degree (X ^ (n - natDegree p)) ≤ ↑n
case mpr.intro.intro.intro.refine'_1
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ degree (p * X ^ (n - natDegree p)) ≤ ↑n
apply le_trans (degree_mul_le _ _) _
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ ↑(natDegree p) + ↑(n - natDegree p) ≤ ↑n
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ degree p + degree (X ^ (n - natDegree p)) ≤ ↑n
apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
no goals
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ ↑(natDegree p) + ↑(n - natDegree p) ≤ ↑n
rw [Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add, this, Nat.cast_withBot]
no goals
case mpr.intro.intro.intro.refine'_2
R : Type u
S : Type ?u.130378
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑n
this : natDegree p + (n - natDegree p) = n
⊢ coeff (p * X ^ (n - natDegree p)) n = Polynomial.leadingCoeff p
rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]