-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_leadingCoeff (x) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x

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

Tactic:
exact ⟨p, hpI, rfl⟩

Result:
no goals

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

Tactic:
constructor

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

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

Proof state:
case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun n => I.leadingCoeffNth n

Tactic:
intro i j

Result:
case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun n => I.leadingCoeffNth n) i) ((fun n => I.leadingCoeffNth n) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun n => I.leadingCoeffNth n) j) ((fun n => I.leadingCoeffNth n) z)

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

Tactic:
rintro ⟨i, p, hpI, _, rfl⟩

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

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
rw [leadingCoeff, Submodule.mem_iSup_of_directed]

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun n => I.leadingCoeffNth n

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
simp only [mem_leadingCoeffNth]

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

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ i, ∃ p_1 ∈ I, p_1.degree ≤ ↑i ∧ p_1.leadingCoeff = p.leadingCoeff

Tactic:
exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩

Result:
no goals

Proof state:
case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun n => I.leadingCoeffNth n) i) ((fun n => I.leadingCoeffNth n) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun n => I.leadingCoeffNth n) j) ((fun n => I.leadingCoeffNth n) z)

Tactic:
exact
  ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
    I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩

Result:
no goals

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

Tactic:
rintro ⟨p, hpI, rfl⟩

Result:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ i, ∃ p_1 ∈ I, p_1.degree ≤ ↑i ∧ p_1.leadingCoeff = p.leadingCoeff