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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ ∃ j ∈ p.support, j + s = m

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 : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) ⇑x ⇑y

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f 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 s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m ((monomial s) r * p) = if s ≤ m then r * coeff (m - s) p 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 σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p 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 σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p 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
p : MvPolynomial σ R
⊢ p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d 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
⊢ p ≠ 0 ↔ ∃ d, coeff d 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
inst✝ : Nontrivial R
s : σ
⊢ X s ≠ 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
⊢ p.support = ∅ ↔ 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
⊢ p.support.Nonempty ↔ p ≠ 0

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
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) 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₁
n : σ
⊢ (map f) (X n) = X 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₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval g) ((map f) 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
ha : IsRegular a
⊢ IsRegular ((MvPolynomial.monomial m) a)

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✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : g wit < f wit
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j wit
⊢ ((ofLex (toLex g)).neLocus (ofLex (toLex f))).min = ↑wit

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✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
⊢ P (toLex f) (toLex g)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (rename f) (C r) = C r

Tactic:
unfold rename C monomial MvPolynomial

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (mapDomainAlgHom R R (mapDomain.addMonoidHom f))
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(AddMonoidAlgebra.lsingle 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      r
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (rename f) (C r) = C r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
i : σ
⊢ (rename f) (X i) = X (f i)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ (map f) ((rename g) (C a)) = (rename g) ((map f) (C a))

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✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ⇑toLex

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p q : MvPolynomial σ R
hp : (map f) ((rename g) p) = (rename g) ((map f) p)
hq : (map f) ((rename g) q) = (rename g) ((map f) q)
⊢ (map f) ((rename g) (p + q)) = (rename g) ((map f) (p + q))

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : (map f) ((rename g) p) = (rename g) ((map f) p)
⊢ (map f) ((rename g) (p * X n)) = (rename g) ((map f) (p * X n))

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ (map f) ((rename g) p) = (rename g) ((map f) p)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (rename g) ((rename f) p) = (rename (g ∘ f)) p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ rename id = AlgHom.id R (MvPolynomial σ R)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (rename id) p = p

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (x✝³ + x✝²)) a) ((ofLex (x✝³ + x✝¹)) a)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ (rename f) ((monomial d) r) = (monomial (Finsupp.mapDomain f d)) r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
⊢ rename f = aeval (X ∘ f)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
⊢ (rename f) p = 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₁
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 (⇑k ∘ g) ((map f) p)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → σ
hf : LeftInverse f g
⊢ LeftInverse ⇑(rename f) ⇑(rename g)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝²)) a)
    ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝¹)) a)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsRegular (X n)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ p.coeffs = ∅

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
⊢ 0 ∈ support 1 ∧ coeff 0 1 = 1

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
⊢ coeffs 1 = {1}

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
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ ((killCompl hf).comp (rename f)) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

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
⊢ 0 ∉ p.coeffs

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 R
r : R
⊢ (C r).coeffs = if r = 0 then ∅ else {r}

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (C r).coeffs ⊆ {r}

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
n : σ
⊢ (p * X n).coeffs = p.coeffs

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
n : σ
⊢ (X n * p).coeffs = p.coeffs

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
⊢ (killCompl hf) ((map φ) p) = (map φ) ((killCompl hf) p)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : σ →₀ ℕ
c : R
⊢ (killCompl hf) ((monomial (Finsupp.mapDomain f s)) c) = (monomial s) c

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ (killCompl hf) ((monomial s) c) = 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 R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
⊢ (killCompl hf) ((monomial s) c) = if ↑s.support ⊆ range f then (monomial (Finsupp.comapDomain f s ⋯)) c 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 R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
x✝ : ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n p ≠ 0
⊢ ¬coeff n p = 0 ∧ r = coeff n p

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
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) 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 R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
x✝ : ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n q ≠ 0
⊢ ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ coeff s ((killCompl hf) p) = coeff (Finsupp.mapDomain f s) p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
⊢ ((killCompl hf) p).support = p.support.preimage (Finsupp.mapDomain f) ⋯

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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
⊢ eval₂ ((map f).comp C) h p = eval₂ C h ((map f) p)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
⊢ (rename ⇑f.symm) ((rename ⇑f) p) = p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
⊢ (rename ⇑f) ((rename ⇑f.symm) p) = p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ ∀ (a : MvPolynomial σ R), (renameEquiv R (Equiv.refl σ)) a = AlgEquiv.refl a

Tactic:
by

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

Goal state before:
pp: S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ q ((eval g) p) = (eval (⇑q ∘ g)) ((map q) p)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) 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 R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n p = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n p = coeff n p + coeff n q

Tactic:
simp [hl n hn, hn]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees = p.support.sup fun s ↦ toMultiset s

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 R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n p = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n p = coeff n p + coeff n q

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ ((monomial s) a).degrees ≤ toMultiset s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p)

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).degrees ≤ p.degrees ⊔ q.degrees

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 R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n q = coeff n p + coeff n q

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
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∑ i ∈ s, f i).degrees ≤ s.sup fun i ↦ (f i).degrees

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) 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 R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
⊢ (p + q).coeffs = p.coeffs ∪ q.coeffs

Tactic:
by

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

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
⊢ coeff 0 1 = 1

Tactic:
by

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

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
⊢ ∀ (x y : MvPolynomial σ R), coeff 0 (x * y) = coeff 0 x * coeff 0 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 q : MvPolynomial σ R
⊢ (p * q).degrees ≤ p.degrees + q.degrees

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ constantCoeff (C r) = r

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ constantCoeff (X 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
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees

Tactic:
by

Goal state after: