R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ leadingCoeffNth I i) ↔ ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x

case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ Directed (fun x x_1 => x ≤ x_1) fun n => leadingCoeffNth I n
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ x ∈ leadingCoeff I ↔ ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x
rw [leadingCoeff, Submodule.mem_iSup_of_directed]
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x) ↔ ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x

case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ Directed (fun x x_1 => x ≤ x_1) fun n => leadingCoeffNth I n
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ leadingCoeffNth I i) ↔ ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x

case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ Directed (fun x x_1 => x ≤ x_1) fun n => leadingCoeffNth I n
simp only [mem_leadingCoeffNth]
case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun n => leadingCoeffNth I n) i) ((fun n => leadingCoeffNth I n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun n => leadingCoeffNth I n) j) ((fun n => leadingCoeffNth I n) z)
case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ Directed (fun x x_1 => x ≤ x_1) fun n => leadingCoeffNth I n
intro i j
no goals
case H
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun n => leadingCoeffNth I n) i) ((fun n => leadingCoeffNth I n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun n => leadingCoeffNth I n) j) ((fun n => leadingCoeffNth I n) z)
exact
  ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
    I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩
case mp
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x) → ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x

case mpr
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x) → ∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x) ↔ ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x
constructor
case mpr.intro.intro
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ i p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑i ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
case mpr
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x) → ∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x
rintro ⟨p, hpI, rfl⟩
no goals
case mpr.intro.intro
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ i p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑i ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩
case mp.intro.intro.intro.intro
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left✝ : degree p ≤ ↑i
⊢ ∃ p_1, p_1 ∈ I ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
case mp
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
⊢ (∃ i p, p ∈ I ∧ degree p ≤ ↑i ∧ Polynomial.leadingCoeff p = x) → ∃ p, p ∈ I ∧ Polynomial.leadingCoeff p = x
rintro ⟨i, p, hpI, _, rfl⟩
no goals
case mp.intro.intro.intro.intro
R : Type u
S : Type ?u.182986
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left✝ : degree p ≤ ↑i
⊢ ∃ p_1, p_1 ∈ I ∧ Polynomial.leadingCoeff p_1 = Polynomial.leadingCoeff p
exact ⟨p, hpI, rfl⟩