awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))

Tactic:
have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
generalize : ∀ (k : ℕ) (hn : p.natDegree = k), 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

Tactic:
generalize hn : p.natDegree = k

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
h₁ : ∀ (h : N < k), 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

Tactic:
rcases le_or_gt k N with h | h

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ ∀ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ p.natDegree ≤ N

Tactic:
subst k
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
h : p.natDegree ≤ N
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p

Tactic:
hs2 ⟨Polynomial.mem_degreeLE.2
            (le_trans Polynomial.degree_le_natDegree <| WithBot.coe_le_coe.2 h), hp⟩

Premises used: Iff.mpr, Set.Mem, Polynomial.degree_le_natDegree, WithBot.coe_le_coe, And.intro, Polynomial.mem_degreeLE, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
h : p.natDegree ≤ N
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p

Tactic:
refine hs2 ⟨Polynomial.mem_degreeLE.2
            (le_trans Polynomial.degree_le_natDegree <| WithBot.coe_le_coe.2 h), hp⟩

Premises used: Iff.mpr, Polynomial.degree_le_natDegree, WithBot.coe_le_coe, And.intro, Polynomial.mem_degreeLE, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ ∀ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ N < natDegree.{u} (R := R) 0

Tactic:
cases hn
-- Module: Mathlib.RingTheory.Polynomial.Basic
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]))
hp : 0 ∈ I
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
h : N < natDegree.{u} (R := R) 0
⊢ False

Tactic:
Nat.not_lt_zero _ h

Premises used: Nat.not_lt_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
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]))
hp : 0 ∈ I
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
h : N < natDegree.{u} (R := R) 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ h

Premises used: Nat.not_lt_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
apply : p = 0
⊢ False

Tactic:
apply hp0
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
a : ∀ (i : ℕ), p.coeff i = coeff 0 i
⊢ p = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
(mul_one _).symm.trans ?_

Premises used: mul_one, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ
a : p.coeff i * 1 = coeff 0 i
⊢ p.coeff i = coeff 0 i

Tactic:
refine (mul_one _).symm.trans ?_

Premises used: mul_one, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ
a : Eq.{u + 1} (α := R) 0 (coeff 0 i)
⊢ p.coeff i * 1 = coeff 0 i

Tactic:
rw [← h, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ
⊢ Eq.{u + 1} (α := R) 0 (coeff 0 i)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := ⟨⟨0, 1, this⟩⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
rw : p.leadingCoeff ∈ M
⊢ p.leadingCoeff ∈ I.leadingCoeffNth N

Tactic:
rw [HN]
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ∈ M

Tactic:
hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)

Premises used: Iff.mpr, Set.Mem, Eq.rec, Polynomial.degree_le_natDegree, Ideal.mem_leadingCoeffNth, And.intro, Exists.intro, rfl