awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
have rw : p.degree = q.degree + (↑(k - q.natDegree) : WithBot ℕ)
Tactic: rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
rw : p.degree = q.degree + (↑(k - q.natDegree) : WithBot ℕ)
⊢ p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
have rw₁ : q.leadingCoeff * (HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff ≠ 0
Tactic: rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ p.degree = q.degree + (↑(k - q.natDegree) : WithBot ℕ)
have rw : (↑p.natDegree : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(k - q.natDegree) : WithBot ℕ)
Tactic: rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(k - q.natDegree) : WithBot ℕ)
have rw : q.natDegree ≤ k
Tactic: rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff * (HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff ≠ 0
have rw : q.leadingCoeff ≠ 0
Tactic: rw [Polynomial.leadingCoeff_X_pow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
Tactic: have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
            rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
            · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
              rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
              · refine le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
            rw [Polynomial.leadingCoeff_X_pow, mul_one]
            exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
⊢ p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
have rw : q.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
Tactic: rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
rw : q.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
⊢ p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
have rw₁ : q.leadingCoeff = q.leadingCoeff
Tactic: rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
Tactic: have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
            rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < p.degree
Tactic: have := Polynomial.degree_sub_lt h1 hp0 h2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < p.degree
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
Tactic: rw [Polynomial.degree_eq_natDegree hp0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h₁ : Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X]))
  (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) + q * HPow.hPow (α := R[X]) X (k - q.natDegree))
Tactic: rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
have pos : ∀ (hpq : p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
  Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
Tactic: by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
pos :
  ∀ (hpq : p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
have neg : ∀ (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
  Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
Tactic: by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
hpq : p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
have pos : Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) 0
Tactic: rw [hpq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))
have neg : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
Tactic: refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl