mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inl
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : k ≤ N
⊢ p ∈ Ideal.span ↑s

pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ∈ Ideal.span ↑s

Tactic:
·

Goal state after:
case h.inl
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : k ≤ N
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ∈ Ideal.span ↑s

Tactic:
·

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
·

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ p.degree = q.degree + ↑(k - q.natDegree)

pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff * (X ^ (k - q.natDegree)).leadingCoeff ≠ 0

Tactic:
·

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ p.degree = q.degree + ↑(k - q.natDegree)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) m

pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) 1

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) m
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) 1

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.natDegree ≤ k

Tactic:
·

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.natDegree ≤ k
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) m

pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) 1

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) m
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) 1

pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
·

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr.convert_2
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

pp: case h.inr.convert_5
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ q ∈ Ideal.span ↑s

Tactic:
·

Goal state after:
case h.inr.convert_2
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (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 = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s