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

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

pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((Finsupp.single i k).prod fun n e ↦ X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1

Tactic:
]

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

R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((Finsupp.single i k).prod fun n e ↦ X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1
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) = coeff m (X i)

Tactic:
]

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

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

Tactic:
]

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

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

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (p.coeff.sum fun n b ↦ (monomial (0 + n)) (a * b)) = a * coeff m p

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
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 ∪ q.support \ p.support ⊆ (p + q).support

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Basic

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

Tactic:
]

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_a.e_a
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
C : σ →₀ ℕ
hc : p.coeff C ≠ 0
i : σ
hi : i ∈ C.support
⊢ coeff C p ≠ 0

Tactic:
]

Goal state after:
case e_a.e_a
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
C : σ →₀ ℕ
hc : p.coeff C ≠ 0
i : σ
hi : i ∈ C.support
⊢ coeff C p ≠ 0
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₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p

Tactic:
]

Goal state after:
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₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff m (p * (monomial s) r)

Tactic:
]

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
⊢ s * (eval x) p = s * (eval x) p

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ s ≤ m

Tactic:
]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ s ≤ m
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₂ ((eval g).comp C) (⇑(eval g) ∘ f) p

Tactic:
]

Goal state after:
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₂ ((eval g).comp C) (⇑(eval g) ∘ f) p
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:
]

Goal state after:
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
Module: Mathlib.Algebra.MvPolynomial.Basic

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

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ∃ d, coeff d (X s) ≠ 0

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ∃ d, coeff d (X s) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ¬p = 0 ↔ p ≠ 0

Tactic:
]

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
⊢ IsLeftRegular ((MvPolynomial.monomial m) a)

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsLeftRegular ((MvPolynomial.monomial m) a)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
d : σ →₀ ℕ
h' : a * coeff d p = a * coeff d q
⊢ a * coeff d q = a * coeff d q

Tactic:
]

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 f)).neLocus (ofLex (toLex g))).min = ↑wit

Tactic:
]

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 (f r) = k (f r)

Tactic:
]

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ

Tactic:
]

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ
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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
hq : k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) + eval₂ k (⇑k ∘ g) ((map f) q) =
    eval₂ k (⇑k ∘ g) ((map f) p) + eval₂ k (⇑k ∘ g) ((map f) q)

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : i ∈ φ.support
⊢ r * C i = r * C i

Tactic:
]

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
⊢ p = 0 ↔ p = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : coeff i φ = 0
⊢ coeff i φ = r * 0

Tactic:
]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : coeff i φ = 0
⊢ coeff i φ = r * 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) * k (g s) = eval₂ k (⇑k ∘ g) ((map f) p) * k (g s)

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : coeff i φ = 0
⊢ coeff i φ = 0

Tactic:
]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : coeff i φ = 0
⊢ coeff i φ = 0
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
⊢ C (f r) = C (f r)

Tactic:
]

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) (X (f i)) = X i

Tactic:
killCompl,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ (aeval fun i ↦ if h : i ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨i, h⟩) else 0) (X (f i)) = X i
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i Q = coeff i Q

Tactic:
]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}
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 : σ
⊢ X i = X i

Tactic:
]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (if r = 0 then ∅ else {r}) ⊆ {r}

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (if r = 0 then ∅ else {r}) ⊆ {r}
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
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✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q) =
    eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q)

Tactic:
]

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:
killCompl,

Goal state after:
σ : 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
⊢ (aeval fun i ↦ if h : i ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨i, h⟩) else 0) ((monomial s) c) = 0
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
⊢ (algebraMap R (MvPolynomial σ R)) c *
      ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a =
    0

Tactic:
]

Goal state after:
σ : 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
⊢ (algebraMap R (MvPolynomial σ R)) c *
      ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a =
    0
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
⊢ (monomial (Finsupp.comapDomain f s ⋯)) c = (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
]

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

Goal state before:
pp: case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
⊢ coeff s (if ↑u.support ⊆ range f then (monomial (Finsupp.comapDomain f u ⋯)) r else 0) =
    coeff (Finsupp.mapDomain f s) ((monomial u) r)

Tactic:
]

Goal state after:
case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
⊢ coeff s (if ↑u.support ⊆ range f then (monomial (Finsupp.comapDomain f u ⋯)) r else 0) =
    coeff (Finsupp.mapDomain f s) ((monomial u) r)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
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✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s)

Tactic:
]

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
⊢ p = p

Tactic:
]

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
⊢ p = p

Tactic:
]

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₁
⊢ eval₂ q (⇑q ∘ g) p = eval₂ q (⇑q ∘ g) p

Tactic:
]

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.support.sup fun s ↦ toMultiset s) = p.support.sup fun s ↦ toMultiset s

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.support.sup fun s ↦ toMultiset s
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).degrees = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ (if d = 0 then r else 0) = if d = 0 then r else 0

Tactic:
]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∑ i ∈ p.support, ((monomial i) (coeff i p)).coeff = p.coeff

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∑ i ∈ p.support, ((monomial i) (coeff i p)).coeff = p.coeff
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s.support = ∅

Tactic:
]

Goal state after:
case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s.support = ∅
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ C r = C r

Tactic:
]

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
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ 0 ≤ (p + q).degrees

Tactic:
]

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ 0 ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d p + coeff d q ≠ 0

Tactic:
]

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d p + coeff d q ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ d ∈ p.coeff.support

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ d ∈ p.coeff.support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
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
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
]

Goal state after:
case refine_1
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
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}
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
hf : LeftInverse ⇑f ⇑g
X : MvPolynomial σ S₁
⊢ X = X

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d.support.Nonempty
⊢ coeff d q = 0

Tactic:
]

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d.support.Nonempty
⊢ coeff d q = 0