R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ leadingCoeffNth I m
⊢ r ∈ leadingCoeffNth I n
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
⊢ leadingCoeffNth I m ≤ leadingCoeffNth I n
intro r hr
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p, p ∈ I ∧ degree p ≤ ↑m ∧ Polynomial.leadingCoeff p = r
⊢ ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = r
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ leadingCoeffNth I m
⊢ r ∈ leadingCoeffNth I n
simp only [SetLike.mem_coe, mem_leadingCoeffNth] at hr⊢
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p, p ∈ I ∧ degree p ≤ ↑m ∧ Polynomial.leadingCoeff p = r
⊢ ∃ p, p ∈ I ∧ degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = r
rcases hr with ⟨p, hpI, hpdeg, rfl⟩
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ degree (p * X ^ (n - m)) ≤ ↑n
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑n ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
refine' ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, _, leadingCoeff_mul_X_pow⟩
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ degree p + degree (X ^ (n - m)) ≤ ↑n
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ degree (p * X ^ (n - m)) ≤ ↑n
refine' le_trans (degree_mul_le _ _) _
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ ↑m + ↑(n - m) ≤ ↑n
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ degree p + degree (X ^ (n - m)) ≤ ↑n
refine' le_trans (add_le_add hpdeg (degree_X_pow_le _)) _
no goals
case intro.intro.intro
R : Type u
S : Type ?u.180424
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑m
⊢ ↑m + ↑(n - m) ≤ ↑n
rw [Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add, add_tsub_cancel_of_le H,
  Nat.cast_withBot]