mathlib-initiative/mathlib-tactics huggingface dataset:
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)

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

Goal state after:
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)

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))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mpr.isTrue
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
i✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h✝ : i✝ ≤ i
⊢ coeff (i - i✝) p * 1 ∈ M

pp: case mpr.isFalse
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
i✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h✝ : ¬i✝ ≤ i
⊢ 0 ∈ M

Tactic:
<;>

Goal state after:
case mpr.isTrue
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
i✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h✝ : i✝ ≤ i
⊢ coeff (i - i✝) p * 1 ∈ M

case mpr.isFalse
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
i✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h✝ : ¬i✝ ≤ i
⊢ 0 ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_1.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∀ a ∈ s, id a ∈ s ∪ t

pp: case add.refine_1.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∀ a ∈ t, id a ∈ s ∪ t

Tactic:
<;>

Goal state after:
case add.refine_1.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∀ a ∈ s, id a ∈ s ∪ t

case add.refine_1.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∀ a ∈ t, id a ∈ s ∪ t
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
⊢ d ∈ (p + q).support

Tactic:
rw [mem_support_iff, coeff_add]

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.Basic

Goal state before:
pp: 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
⊢ coeffsIn σ M = Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
refine le_antisymm ?_ <| Submodule.span_le.2 ?_

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
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

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
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2.isTrue
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 : σ →₀ ℕ
h✝ : s = i
⊢ m ∈ M

pp: case refine_2.isFalse
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 : σ →₀ ℕ
h✝ : ¬s = i
⊢ 0 ∈ M

Tactic:
<;>

Goal state after:
case refine_2.isTrue
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 : σ →₀ ℕ
h✝ : s = i
⊢ m ∈ M

case refine_2.isFalse
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 : σ →₀ ℕ
h✝ : ¬s = i
⊢ 0 ∈ M
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₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval g) ((map f) (C a)) = eval₂ f g (C a)

pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval g) ((map f) p) = eval₂ f g p →
      (eval g) ((map f) q) = eval₂ f g q → (eval g) ((map f) (p + q)) = eval₂ f g (p + q)

pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g) ((map f) p) = eval₂ f g p → (eval g) ((map f) (p * X n)) = eval₂ f g (p * X n)

Tactic:
<;>

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval g) ((map f) (C a)) = eval₂ f g (C a)

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval g) ((map f) p) = eval₂ f g p →
      (eval g) ((map f) q) = eval₂ f g q → (eval g) ((map f) (p + q)) = eval₂ f g (p + q)

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g) ((map f) p) = eval₂ f g p → (eval g) ((map f) (p * X n)) = eval₂ f g (p * X n)
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✝ : Module R S
M : Submodule R S
N : Submodule R (MvPolynomial σ S)
⊢ coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ N

Tactic:
simp [coeffsIn_eq_span_monomial, Submodule.span_le, Set.subset_def,
    forall_comm (α := MvPolynomial σ S)]

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

Goal state before:
pp: case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₁)

pp: case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₂)

Tactic:
<;>

Goal state after:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₁)

case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₂)
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✝

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

Goal state after:
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✝

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✝)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1.mem_mul_mem.hm
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m ∈ coeffsIn σ M

pp: case hn
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial 0) n ∈ coeffsIn σ N

Tactic:
<;>

Goal state after:
case refine_1.mem_mul_mem.hm
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m ∈ coeffsIn σ M

case hn
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial 0) n ∈ coeffsIn σ N
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ (a ≠ 0 ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
eq_true ha,

Goal state after:
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ (True ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p - q = p + -q

pp: case e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ q.vars = (-q).vars

Tactic:
<;>

Goal state after:
case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p - q = p + -q

case e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ q.vars = (-q).vars
Module: Mathlib.Algebra.MvPolynomial.CommRing

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

pp: case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ q.vars = (-q).vars

Tactic:
<;>

Goal state after:
case e'_2
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ p - q = p + -q

case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ q.vars = (-q).vars
Module: Mathlib.Algebra.MvPolynomial.Eval

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

pp: case hX
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
i✝ : σ
⊢ (eval₂Hom f 0) (X i✝) = (f.comp constantCoeff) (X i✝)

Tactic:
<;>

Goal state after:
case hC
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
x✝ : R
⊢ ((eval₂Hom f 0).comp C) x✝ = ((f.comp constantCoeff).comp C) x✝

case hX
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
i✝ : σ
⊢ (eval₂Hom f 0) (X i✝) = (f.comp constantCoeff) (X i✝)
Module: Mathlib.Data.Finsupp.Fin

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

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

Tactic:
<;>

Goal state after:
case zero
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
⊢ (cons y 0) 0 = (single 0 y) 0

case succ
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
i✝ : Fin n
⊢ (cons y 0) i✝.succ = (single 0 y) i✝.succ
Module: Mathlib.Data.Finsupp.Fin

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

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

Tactic:
<;>

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

case succ
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
i✝ : Fin n
⊢ (cons 0 (single i y)) i✝.succ = (single i.succ y) i✝.succ
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
h0,

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
rw [h0, f.map_zero, Finset.sum_eq_zero]

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ ∀ x ∈ p.support, (f (coeff x p) * x.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ i ∈ p.vars

Tactic:
mem_vars_iff_mem_support

Goal state after:
case pos.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ (Finset.cons a s has).sup fun i ↦ (f i).totalDegree

Tactic:
Finset.sup_cons

Goal state after:
case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun i ↦ (f i).totalDegree)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ i ∈ p.vars

Tactic:
mem_vars_iff_mem_support

Goal state after:
case neg.h₀.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 → p = C (coeff 0 p)

pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = C (coeff 0 p) → p.totalDegree = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 → p = C (coeff 0 p)

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = C (coeff 0 p) → p.totalDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ i ∈ p₁.vars

Tactic:
mem_vars_iff_mem_support

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p₁.support, i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X.inl
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inl val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inl val✝)))

pp: case mul_X.inr
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inr val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inr val✝)))

Tactic:
<;>

Goal state after:
case mul_X.inl
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inl val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inl val✝)))

case mul_X.inr
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inr val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inr val✝)))
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ (f₁.comp C) x✝ = ((eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)).comp C) x✝

pp: case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ f₁ (X i✝) = (eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)) (X i✝)

Tactic:
<;>

Goal state after:
case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ (f₁.comp C) x✝ = ((eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)).comp C) x✝

case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ f₁ (X i✝) = (eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ ((eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)).comp C) x✝ = (f₂.comp C) x✝

pp: case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ (eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)) (X i✝) = f₂ (X i✝)

Tactic:
<;>

Goal state after:
case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ ((eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)).comp C) x✝ = (f₂.comp C) x✝

case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ (eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)) (X i✝) = f₂ (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : ¬a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

case neg
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : ¬a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a