mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ (P * Q).coeff (l + m) = 0

Tactic:
hQ,

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ coeff 0 (l + m) = 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f - g).neLocus f = g.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ (l, m) ∉ antidiagonal (l + m) → P.coeff (l, m).1 * Q.coeff (l, m).2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ m < j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ Q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∉ R[X]⁰ ↔ ∃ a, a ≠ 0 ∧ a • P = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hp : p.coeff n ∈ R⁰
r : R
hr : r • p = 0
⊢ r * p.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.coeff 1 ∈ R⁰

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✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ eval₂ g X f = ∑ d ∈ f.support, g (coeff d f) * ∏ i, X i ^ d 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₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ (coeffEquiv.toFun p).support ∪ (coeffEquiv.toFun q).support, (f 0 * a.prod fun n e ↦ g n ^ e) = 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₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ (coeffEquiv.toFun p).support ∪ (coeffEquiv.toFun q).support,
    ∀ (b₁ b₂ : R),
      (f (b₁ + b₂) * a.prod fun n e ↦ g n ^ e) = (f b₁ * a.prod fun n e ↦ g n ^ e) + f b₂ * a.prod fun n e ↦ g n ^ e

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₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ (f 0 * s.prod fun n e ↦ g n ^ e) = 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₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g (C a) = f a

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₁
g : σ → S₁
n : σ
⊢ eval₂ f g (X n) = g n

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₁
g : σ → S₁
s : σ
n : ℕ
⊢ eval₂ f g (X s ^ n) = g s ^ n

Tactic:
by

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

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]

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

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ C a * (monomial s) a' = (monomial s) (a * a')

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
inst✝ : CommSemiring R
⊢ C (a + a') = C a + C a'

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ C (p.coeff 0) = p

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ C ↑n = ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = a • 1

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
e : ℕ
n : σ
inst✝ : CommSemiring R
⊢ X n ^ e = (monomial (Finsupp.single n e)) 1

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial s) a * X n ^ e

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (Finsupp.single n e + s)) a = X n ^ e * (monomial s) a

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (Finsupp.single s n)) a

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = (monomial (Finsupp.single s 1)) a

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₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (monomial (Finsupp.single n 1 + s)) a)

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₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * (monomial (Finsupp.single n 1 + s)) a) =
    eval₂ f g (p * (monomial (Finsupp.single n 1)) 1) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ (monomial (∑ i ∈ s, f i)) a = C a * ∏ i ∈ s, (monomial (f i)) 1

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ (monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i) = ∏ i ∈ s, (monomial (f i)) (g i)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial s) a = C a * s.prod fun n e ↦ X n ^ e

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∏ x ∈ s.support, X x ^ s x = (monomial s) 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₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
a : R
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ (eval₂ f g p * f a * Finsupp.prod 0 fun n e ↦ g n ^ e) = eval₂ f g p * f a

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
x✝ : σ
hi : x✝ ∈ t
⊢ X x✝ ^ x x✝ = X x✝ ^ (Finsupp.indicator t fun i x_1 ↦ x i) x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∏ y ∈ t, X y ^ x y = (monomial (Finsupp.indicator t fun i x_1 ↦ 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₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

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₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
hp : eval₂ f g p = 0
⊢ eval₂ f g (p * q) = 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₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
hq : eval₂ f g q = 0
⊢ eval₂ f g (p * q) = 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₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g (p ^ 0) = eval₂ f g p ^ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p) a)
⊢ ∀ (e : ℕ), motive ((monomial p) a * X n ^ e)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
⊢ ∀ (s : σ →₀ ℕ) (a : R), motive ((monomial s) a)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)
add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P ((MvPolynomial.monomial 0) 0)
⊢ P 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₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 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₁ f₂ : R →+* S₁
g₁ g₂ : σ → S₁
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₂ g₂) p₂

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : MvPolynomial σ R →ₐ[R] A
hf : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroAlgHom = g.comp singleZeroAlgHom

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Algebra.adjoin R (range X) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).support = {Finsupp.single n 1}

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₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i ↦ φ (g i)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).support = {Finsupp.single s n}

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ support 1 = {0}

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
α : Type u_2
inst✝ : DecidableEq σ
s : Finset α
f : α → MvPolynomial σ R
⊢ (∑ x ∈ s, f x).support ⊆ s.biUnion fun x ↦ (f x).support

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support ↔ coeff m p ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∉ p.support ↔ coeff m p = 0

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₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) p

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₁
g : σ → S₁
d : σ →₀ ℕ
r : R
⊢ (eval₂Hom f g) ((monomial d) r) = f r * d.prod fun i k ↦ g i ^ k

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : AddCommMonoid A
p : MvPolynomial σ R
b : (σ →₀ ℕ) → R → A
⊢ p.coeff.sum b = ∑ m ∈ p.support, b m (coeff m p)

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₁
g : σ → S₁
r : R
P : MvPolynomial σ R
⊢ (eval₂Hom f g) (r • P) = f r • (eval₂Hom f g) P

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ Disjoint ((monomial a) s).support p.support

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
⊢ p.coeff = q.coeff

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
p q : MvPolynomial σ R
⊢ coeff m (p + q) = coeff m p + coeff m q

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
h : Finsupp.single i 1 = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
⊢ (monomial m) 1 = m.prod fun n e ↦ X n ^ e

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a ↦ toLex (single a 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
⊢ φ = (monomial d₀) (coeff d₀ φ)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
h : m ≠ 0
a : R
⊢ coeff m (C a) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : NeZero n
m : σ →₀ ℕ
a : R
i : σ
H : m + Finsupp.single i n = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ p = C (coeff 0 p)

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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = if Finsupp.single i 1 = m then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ coeff (Finsupp.single i 1) (X i) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ eval₂ C X p = p

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (C a * p) = a * coeff m p

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n n' : ℕ
⊢ coeff (Finsupp.single s' n') (X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n : ℕ
⊢ coeff (Finsupp.single s' n) (X s) = if n = 1 ∧ s = s' then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ coeff d (∏ y ∈ s, X y ^ x y) = if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), y * 1 = 0 ↔ y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), 1 * y = 0 ↔ y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support ∆ q.support ⊆ (p + q).support

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₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
⊢ eval₂ f g₁ p = eval₂ f g₂ 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₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t ↦ eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x) (s • p) = s * (eval x) p

Tactic:
by

Goal state after: