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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
a✝ : A[X]
n✝ : ℕ
⊢ (((mapAlgEquiv f).trans (mapAlgEquiv g)) a✝).coeff n✝ = ((mapAlgEquiv (f.trans g)) a✝).coeff n✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
i : ι
x : α
f : ι →₀ α
⊢ (∀ i_1 ∈ {i}, (single i x) i_1 ≤ f i_1) ↔ x ≤ f i

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X + C t).comp (X - C t) = X

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X - C t).comp (X + C t) = X

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
⊢ (-X).comp (-X) = X

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ x✝ ∈ ↑y.support → x✝ ∈ ↑(y + w).support

Tactic:
simp

Goal state after:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ ¬y x✝ = 0 → y x✝ = 0 → ¬w x✝ = 0
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i

Tactic:
exact ⟨j, hl, hj⟩

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i

Tactic:
exact ⟨j, hl, hj⟩

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

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
⊢ X ^ k • (rTensor N (↑R (monomial 0))) 0 = (rTensor N (↑R (monomial k))) 0

Tactic:
simp

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

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ ∀ i_1 ∈ f.support.erase i, p ∣ (RingHom.id S) (f.coeff i_1) * z ^ i_1

Tactic:
intro j

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
j : ℕ
⊢ j ∈ f.support.erase i → p ∣ (RingHom.id S) (f.coeff j) * z ^ j
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ (∀ i_1 ∈ {i}, (single i a) i_1 ≤ f i_1) ↔ a ≤ f i

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r p * r = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ Commute r r

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a b : α i✝
inst✝ : ∀ (i : ι), AddLeftMono (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
i : ι
⊢ g i = (f + (g - f)) i

Tactic:
exact (add_tsub_cancel_of_le <| h i).symm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support

Tactic:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case hC
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₂
x✝ : R
⊢ ((φ.comp (eval₂Hom f g)).comp C) x✝ = ((eval₂Hom (φ.comp f) fun i ↦ φ (g i)).comp C) x✝

Tactic:
simp

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

Goal state before:
pp: case hX
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₂
i✝ : σ
⊢ (φ.comp (eval₂Hom f g)) (X i✝) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) (X i✝)

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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:
classical rw [coeff_X, if_pos rfl]

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
⊢ (p.coeff.sum fun n b ↦ (monomial (0 + n)) (0 * b)) = 0

Tactic:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case e_f
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
a : R
⊢ f a = ((eval₂Hom f g).comp C) a

Tactic:
simp

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

Goal state before:
pp: case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ (RingHom.id R) a = ((eval₂Hom (RingHom.id R) g).comp C) a

Tactic:
simp

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

Goal state before:
pp: case C
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
⊢ ∀ (a : R), (eval x) (eval₂ f g (C a)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (C a)

Tactic:
simp

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:
neLocus_comm

Goal state after:
ι : 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 f)).neLocus (ofLex (toLex g))).min = ↑wit
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
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
r : R
⊢ k (eval₂ f g (C r)) = eval₂ k (⇑k ∘ g) ((map f) (C r))

Tactic:
eval₂_C,

Goal state after:
case C
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
r : R
⊢ k (f r) = eval₂ k (⇑k ∘ g) ((map f) (C 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
⊢ (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

Tactic:
simp

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:
simp

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✝ : σ
m✝ : τ →₀ ℕ
⊢ coeff m✝ ((rename f) (X i✝)) = coeff m✝ ((aeval (X ∘ f)) (X i✝))

Tactic:
simp

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

Goal state before:
pp: case C
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
r : R
⊢ (map f) (eval₂ C g (C r)) = eval₂ C (⇑(map f) ∘ g) ((map f) (C r))

Tactic:
eval₂_C,

Goal state after:
case C
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
r : R
⊢ (map f) (C r) = eval₂ C (⇑(map f) ∘ g) ((map f) (C r))
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:
simp

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

Goal state before:
pp: case isTrue
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : r = 0
⊢ ∅ ⊆ {r}

Tactic:
simp

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

Goal state before:
pp: case isFalse
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : ¬r = 0
⊢ {r} ⊆ {r}

Tactic:
simp

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

Goal state before:
pp: case hC
σ : 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
i : R
n : σ →₀ ℕ
⊢ coeff n ((((↑(killCompl hf)).comp (map φ)).comp C) i) = coeff n ((((map φ).comp ↑(killCompl hf)).comp C) i)

Tactic:
simp

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

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
⊢ ↑(Finset.image f s.support) ⊆ range f

Tactic:
simp

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:
simp

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:
simp

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✝
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ 0 ∈ {p | ∀ (i : σ →₀ ℕ), coeff i p ∈ M}

Tactic:
simp

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

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : R
x : σ →₀ ℕ
⊢ coeff x (((map f).comp C) a) = coeff x (((eval₂Hom (C.comp f) X).comp C) a)

Tactic:
simp

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

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ
x : σ →₀ ℕ
⊢ coeff x ((map f) (X a)) = coeff x ((eval₂Hom (C.comp f) X) (X a))

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ coeff i ((monomial s) m) ∈ M

Tactic:
simp

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ (if s = i then m else 0) ∈ M
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
x✝ : R
⊢ ((constantCoeff.comp (map f)).comp C) x✝ = ((f.comp constantCoeff).comp C) x✝

Tactic:
simp

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

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
i✝ : σ
⊢ (constantCoeff.comp (map f)) (X i✝) = (f.comp constantCoeff) (X i✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : 1 ≠ 0
M : Submodule R S
⊢ coeffsIn σ (M ^ 1) = coeffsIn σ M ^ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∀ x_1 ∈ x.support, (Finsupp.single (f x_1) (x x_1)) i = 0

Tactic:
intro j

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
j : σ
⊢ j ∈ x.support → (Finsupp.single (f j) (x j)) i = 0
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₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Finset.image (⇑f) ((monomial a) s).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs ∪ Finset.image (⇑f) p.coeffs

Tactic:
simp

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₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Finset.image (⇑f) p.coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs ∪ Finset.image (⇑f) p.coeffs

Tactic:
simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ (C (coeff 0 p)).vars = ∅

Tactic:
simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
a✝ : σ →₀ ℕ
⊢ a✝ ∈ (-p).support ↔ a✝ ∈ p.support

Tactic:
simp

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₁
p : MvPolynomial σ R
⊢ ⇑f '' ↑p.coeffs ⊆ range ⇑f

Tactic:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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
  rw [degrees, support_neg]; rfl

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₁
i : σ
⊢ φ (X i) = (aeval (⇑φ ∘ X)) (X i)

Tactic:
simp

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:
ext i
  simp

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
i : σ
⊢ (φ.comp (aeval f)) (X i) = (aeval fun i ↦ φ (f i)) (X i)

Tactic:
simp

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:
ext i
  simp

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

Goal state before:
pp: case empty
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 ∈ ∅, φ i).vars = ∅.biUnion fun i ↦ (φ i).vars

Tactic:
simp

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

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

Tactic:
rw [pow_zero, mul_one, add_zero]

Goal state after: