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
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

Tactic:
have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
            rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
-- 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
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
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < p.degree

Tactic:
have := Polynomial.degree_sub_lt h1 hp0 h2
-- 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_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
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)

Tactic:
rw [Polynomial.degree_eq_natDegree hp0] at this

Premises used: Polynomial.degree_eq_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_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 ℕ)
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))
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p

Tactic:
rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, Polynomial.natDegree, Polynomial.X, sub_add_cancel
-- 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_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) + q * HPow.hPow (α := R[X]) X (k - q.natDegree))

Tactic:
(Ideal.span ↑s).add_mem _ ((Ideal.span (s : Set R[X])).mul_mem_right _ _)

Premises used: Ideal.add_mem, SetLike.coe, Ideal.mul_mem_right, Ideal.span
-- 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_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))
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))
⊢ 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

Premises used: HSub.hSub, Polynomial.natDegree, Polynomial.X
-- 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_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
pos : Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) 0
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))

Tactic:
rw [hpq]
-- 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_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])) 0

Tactic:
Ideal.zero_mem _

Premises used: Set.Mem, Ideal.zero_mem
-- 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_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])) 0

Tactic:
exact Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- 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_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))

Tactic:
ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl

Premises used: Set.Mem, Ideal.mul_mem_right, Ideal.sub_mem, 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_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
neg : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree))

Tactic:
refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl

Premises used: Ideal.mul_mem_right, Ideal.sub_mem, 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_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
neg :
  ∀
    (this :
      LT.lt (α := WithBot ℕ) (↑(p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree : WithBot ℕ)
        (↑p.natDegree : WithBot ℕ))
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
neg₁ :
  ∀ (this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < p.natDegree)
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
neg₂ neg₃ neg₄ neg₅ :
  ∀ (this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k)
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k

Tactic:
rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt
-- 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_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])) q

Tactic:
hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

Premises used: Iff.mpr, And.intro, Polynomial.mem_degreeLE
-- 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_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])) q

Tactic:
exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

Premises used: Iff.mpr, And.intro, Polynomial.mem_degreeLE
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
rw :
  (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) ((Finsupp.linearCombination R fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v : (a : ℕ →₀ R) → M) l : M)
          (0 : M) →
        l = 0) ↔
    ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0
⊢ (LinearIndependent.{0, u, w} R (M := M) fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v) ↔
    ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0

Tactic:
rw [linearIndependent_iff]

Premises used: linearIndependent_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
simp :
  (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) (l.sum fun (i : ℕ) (a : R) ↦ HSMul.hSMul (β := M) a ((f ^ i : (a : M) → M) v : M)) 0 →
        l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ),
      Eq.{w + 1} (α := M)
          ({ toFinsupp := q : R[X] }.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M)) 0 →
        q = 0
⊢ (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) ((Finsupp.linearCombination R fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v : (a : ℕ →₀ R) → M) l : M)
          (0 : M) →
        l = 0) ↔
    ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0

Tactic:
simp only [Finsupp.linearCombination_apply, aeval_endomorphism, forall_iff_forall_finsupp,
    ofFinsupp_eq_zero]

Premises used: Finsupp.linearCombination_apply, Polynomial.aeval_endomorphism, Polynomial.ofFinsupp_eq_zero, Polynomial.forall_iff_forall_finsupp