mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
⊢ degreeOf i (X i) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hx : ↑(C 0).coeffs ⊆ range ⇑f
⊢ (map f) 0 = C 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ degreeOf i p ≠ 0 → p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint p.vars q.vars
⊢ (p + q).vars = p.vars ∪ q.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
b : R
h : ¬f b = 0
⊢ (map f) (C b) = C (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
n : σ
q : MvPolynomial σ R
ih : ↑((map f) q).coeffs ⊆ range ⇑f → (map f) q ∈ range ⇑(map f)
hx : ↑((map f) q).coeffs ⊆ range ⇑f
⊢ (map f) (q * X n) = (map f) q * X n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ degreeOf i f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf i ((monomial s) a) = s i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
k : ℕ
⊢ degreeOf i (X i ^ k) = k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑((monomial a) s).coeffs ⊆ range ⇑f ∧ ↑p.coeffs ⊆ range ⇑f
q : MvPolynomial σ R
hq : (map f) q = (monomial a) s
u : MvPolynomial σ R
hu : (map f) u = p
⊢ (map f) (q + u) = (monomial a) s + p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).vars ⊆ s.biUnion fun i ↦ (f i).vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ s i ≤ degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : degreeOf i p < s i
⊢ s ∉ p.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
⊢ x ∈ range ⇑(map f) ↔ ↑x.coeffs ⊆ range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j ↦ degreeOf i (f j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ (C a * φ).vars = φ.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
inst✝ : Algebra R S₁
g : σ → S₁
r : R
⊢ (↑↑(eval₂Hom (algebraMap R S₁) g)).toFun ((algebraMap R (MvPolynomial σ R)) r) = (algebraMap R S₁) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : ¬c = 0
h2 : x ∈ {d'}
⊢ x ∈ {d'}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ (a1 a2 : σ →₀ ℕ), (a1 + a2) i = a1 i + a2 i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ (p - ((monomial d) c - (monomial d') c)).support ⊆ p.support.erase d ∪ {d'}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).degrees = p.degrees

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p - q).degrees ≤ p.degrees ∪ q.degrees

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ degreeOf i (-p) = degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ Subalgebra.toSubmodule (mapAlgHom f).range = coeffsIn σ (Subalgebra.toSubmodule f.range)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).vars = p.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (p - q).vars ⊆ p.vars ∪ q.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
⊢ φ = aeval (⇑φ ∘ X)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
⊢ φ.comp (aeval f) = aeval fun i ↦ φ (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (⇑f ∘ X) (C n) = f (C n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (X j ^ k) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = (aeval fun i ↦ φ (f i)) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
⊢ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ eval₂ c (⇑f ∘ X) (p + q) = f (p + q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i ↦ (φ i).vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun i ↦ φ (g i)) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ eval₂ c (⇑f ∘ X) (p * X n) = f (p * X n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
⊢ eval₂ c (⇑f ∘ X) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : CommRing S
f✝ : R →+* S
g f : σ → S
x : σ
⊢ (fun f ↦ ⇑f ∘ X) ((fun f ↦ eval₂Hom (Int.castRingHom S) f) f) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a : MvPolynomial σ R
⊢ (-a).totalDegree = a.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ (a - b).totalDegree = (a + -b).totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
i : σ
⊢ (aeval f).toRingHom (X i) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ (aeval f).range = Algebra.adjoin R (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree (C r).totalDegree = p.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
⊢ (∑ i ∈ t, φ i).vars = t.biUnion fun i ↦ (φ i).vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).vars ⊆ p.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
⊢ eval₂Hom f 0 = f.comp constantCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
hf : Injective ⇑f
⊢ ((map f) p).vars = p.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ ((monomial (Finsupp.single i e)) r).vars = {i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
⊢ p * X i ^ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
k : Fin n
⊢ (cons y s).tail k = s k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update 0 y).tail = t.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update i.succ y).tail = t.tail.update i y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
⊢ cons (t 0) t.tail = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
⊢ cons y 0 = single 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
⊢ cons 0 (single i y) = single i.succ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ cons 0 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p.vars = p.support.biUnion Finsupp.support

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : y ≠ 0
⊢ cons y s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : s ≠ 0
⊢ cons y s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
this : i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
k : ℕ
h : p ≠ 0
⊢ degreeOf i (p * X i ^ k) = degreeOf i p + k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ (cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ Injective2 cons

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (p * X j ^ k) = degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) φ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Algebra.adjoin R (range f) = (aeval f).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = (aeval Subtype.val).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S₁
p q : MvPolynomial σ R
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : CommSemiring B
inst✝² : Algebra S R
inst✝¹ : Algebra S A
inst✝ : Algebra S B
f : R →ₐ[S] A
X : σ → A
r : S
⊢ (↑↑(eval₂Hom (↑f) X)).toFun ((algebraMap S (MvPolynomial σ R)) r) = (algebraMap S A) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ((cons i σ).sum fun x e ↦ e) = i + σ.sum fun x e ↦ e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x✝ : Fin (n + 1)
⊢ f x✝ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x✝ : Fin n
⊢ Fin.tail f x✝ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: n : Fin 2 →₀ ℕ
⊢ ofSupportFinite ![n 0, n 1] ⋯ = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
d : M × M
inst✝ : AddCommMonoid M
⊢ (((finTwoArrowEquiv' M).symm d).sum fun x n ↦ n) = d.1 + d.2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
⊢ aevalTower (Algebra.ofId S A) = aeval

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ p.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ degreeOf i p ≤ s i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ s ∉ q.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ ∀ (i : σ →₀ ℕ), f (coeff i p) ∈ s

Tactic:
by

Goal state after: