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 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
p : R[X]
hp : p ∈ I
k : ℕ
hn : p.natDegree = k
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h : ∀ (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),
  Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: induction k using Nat.strong_induction_on generalizing p with | _ k ih
Cleared hypotheses: p, hp, k, 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 : 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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h : ∀ (h : k ≤ N), Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: rcases le_or_gt k N with h | h
-- 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 : 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 : ∀ (h : k ≤ N), Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h₁ : ∀ (h : N < k), Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: rcases le_or_gt k N with h | h
-- 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 : 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 : k ≤ N
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have ih₁ : ∀ m < p.natDegree,
  ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
    Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: subst k
Cleared hypotheses: k, ih, hn, h
-- 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 : 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 : k ≤ N
ih₁ :
  ∀ m < p.natDegree,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h₁ : p.natDegree ≤ N
Tactic: subst k
Cleared hypotheses: k, ih, hn, h
-- 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 : 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
h : N < k
hp : 0 ∈ I
hn : natDegree.{u} (R := R) 0 = k
⊢ False
have ih₁ : ∀ m < natDegree.{u} (R := R) 0,
  ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
    Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: cases hn
Cleared hypotheses: k, ih, h, hn
-- 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 : 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
h : N < k
hp : 0 ∈ I
hn : natDegree.{u} (R := R) 0 = k
ih₁ :
  ∀ m < natDegree.{u} (R := R) 0,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
⊢ False
have h₁ : N < natDegree.{u} (R := R) 0
Tactic: cases hn
Cleared hypotheses: k, ih, h, hn
-- 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 : 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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h
-- 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 : 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_1 : N < k
hp0 : p ≠ 0
h : Eq.{u + 1} (α := R) 0 1
⊢ False
have apply : p = 0
Tactic: apply hp0
-- 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 : 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_1 : N < k
hp0 : p ≠ 0
h : Eq.{u + 1} (α := R) 0 1
⊢ p = 0
have a : ∀ (i : ℕ), p.coeff i = coeff 0 i
Tactic: ext i
-- 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 : 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_1 : N < k
hp0 : p ≠ 0
h : Eq.{u + 1} (α := R) 0 1
i : ℕ
⊢ p.coeff i = coeff 0 i
have a : p.coeff i * 1 = coeff 0 i
Tactic: refine (mul_one _).symm.trans ?_
-- 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 : 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_1 : N < k
hp0 : p ≠ 0
h : Eq.{u + 1} (α := R) 0 1
i : ℕ
⊢ p.coeff i * 1 = coeff 0 i
have a : Eq.{u + 1} (α := R) 0 (coeff 0 i)
Tactic: rw [← h, mul_zero]
-- 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 : 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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : Ne.{u + 1} (α := R) 0 1
Tactic: have : (0 : R) ≠ 1 := by
            intro h
            apply hp0
            ext i
            refine (mul_one _).symm.trans ?_
            rw [← h, mul_zero]
            rfl
-- 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 : Ne.{u + 1} (α := R) 0 1
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : Nontrivial R
Tactic: haveI : Nontrivial R := ⟨⟨0, 1, 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 : Nontrivial R
⊢ p.leadingCoeff ∈ I.leadingCoeffNth N
have rw : p.leadingCoeff ∈ M
Tactic: rw [HN]
-- 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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : p.leadingCoeff ∈ I.leadingCoeffNth N
Tactic: have : p.leadingCoeff ∈ I.leadingCoeffNth N := by
            rw [HN]
            exact hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
-- 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
this : p.leadingCoeff ∈ I.leadingCoeffNth N
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have this₁ : ∃ p_1 ∈ I, p_1.degree ≤ (↑N : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff
Tactic: rw [I.mem_leadingCoeffNth] 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
this : ∃ p_1 ∈ I, p_1.degree ≤ (↑N : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have h₁ : ∀ (q : R[X]) (hq : q ∈ I) (hdq : q.degree ≤ (↑N : WithBot ℕ)) (hlqp : q.leadingCoeff = p.leadingCoeff),
  Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: rcases this with ⟨q, hq, hdq, hlqp⟩
Cleared hypotheses: this
-- 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
H : q = 0
⊢ False
have H₁ : q.leadingCoeff = 0
Tactic: rw [← Polynomial.leadingCoeff_eq_zero] at H
Cleared hypotheses: H
-- 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
H : q.leadingCoeff = 0
⊢ False
have H₁ : p = 0
Tactic: rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
Cleared hypotheses: H
-- 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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have hq0 : q ≠ 0
Tactic: have hq0 : q ≠ 0 := by
            intro H
            rw [← Polynomial.leadingCoeff_eq_zero] at H
            rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
            exact hp0 H