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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

pp: case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun n ↦ I.leadingCoeffNth n

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun n ↦ I.leadingCoeffNth n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ ⊤

Tactic:
]

Goal state after:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ antidiagonal k, (f a).coeff x.1 * (∏ x ∈ s, f x).coeff x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
]

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ antidiagonal k, (f a).coeff x.1 * (∏ x ∈ s, f x).coeff x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)

Tactic:
]

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.zero
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
⊢ x ∈ P

Tactic:
]

Goal state after:
case mp.zero
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
⊢ x ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∃ x, coeff 1 x ∉ P

Tactic:
]

Goal state after:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∃ x, coeff 1 x ∉ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P

pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P

Tactic:
]

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P

R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P

Tactic:
]

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P

Tactic:
]

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hzero : f.eraseLead = 0
⊢ C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)

Tactic:
]

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hzero : f.eraseLead = 0
⊢ C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ (f.sum fun n a ↦ C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ (f.sum fun n a ↦ C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ ∃ i, C (f.coeff n) = C (f.coeff i)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ ∃ i, C (f.coeff n) = C (f.coeff i)
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = C (f.coeff n) * X ^ n

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

pp: R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r

Tactic:
]

Goal state after:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ 0 = C 0

Tactic:
]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ 0 = C 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.42

Tactic:
]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.42
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial (↥s) R)) r ∣ a' * b'
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'

Tactic:
]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial (↥s) R)) r ∣ a' * b'
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : FiniteType R S
⊢ S[ X] = ⊤

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : FiniteType R S
⊢ S[ X] = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range MvPolynomial.X) = ⊤

Tactic:
]

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range MvPolynomial.X) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range (FreeAlgebra.ι S)) = ⊤

Tactic:
]

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range (FreeAlgebra.ι S)) = ⊤
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
⊢ I ≤ Ideal.span ↑s

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
⊢ I ≤ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Set.univ = Set.univ

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ ⊤

Tactic:
]

Goal state after:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f

Tactic:
]

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x✝ : R
⊢ MulOpposite.op ((algebraMap R A) x✝) = x ↔ MulOpposite.op ((algebraMap R A) x✝) = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f

Tactic:
]

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → ∃ n f, Surjective ⇑f

Tactic:
]

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → ∃ n f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ (⊤.prod ⊤).FG

Tactic:
]

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ (⊤.prod ⊤).FG
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ (adjoin R t).FG

Tactic:
]

Goal state after:
R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ (adjoin R t).FG
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FiniteType A B ↔ Algebra.FiniteType A B

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ (f.comp (RingHom.id A)).FiniteType

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ (f.comp (RingHom.id A)).FiniteType
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support) = ⊤

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤
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
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i

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
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i