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

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0

pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
leadingCoeff_mul',

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = q.leadingCoeff

case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
leadingCoeff_mul',

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = p.leadingCoeff

R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (C a * 0).degree = degree 0

pp: case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
· simp

Goal state after:
case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (C a * p).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ 0 + p.degree = p.degree

pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
· simp

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (0 * C a).degree = degree 0

pp: case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (p * C a).degree = p.degree

Tactic:
· simp

Goal state after:
case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (p * C a).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + 0 = p.degree

pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0

Tactic:
· simp

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ (0 * q).coeff (Function.invFun D (supDegree D 0 + supDegree D q)) = leadingCoeff D 0 * leadingCoeff D q

pp: case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ (p * 0).coeff (Function.invFun D (supDegree D p + supDegree D 0)) = leadingCoeff D p * leadingCoeff D 0

pp: case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp✝ : p ≠ 0
hq✝ : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) =
    p.coeff (Function.invFun D (supDegree D p)) * q.coeff (Function.invFun D (supDegree D q))

Tactic:
hp,

Goal state after:
case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp✝ : p ≠ 0
hq✝ : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (Function.invFun D (D ap + supDegree D q)) =
    p.coeff (Function.invFun D (D ap)) * q.coeff (Function.invFun D (supDegree D q))
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h✝ : Nontrivial R
⊢ ¬p = 0

Tactic:
hp,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h✝ : Nontrivial R
⊢ ¬False
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Semiring S
c : S
a✝ : Nontrivial S
⊢ (X + C c).nextCoeff = c

Tactic:
simp [nextCoeff_of_natDegree_pos]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
hp,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ 1 * leadingCoeff D q ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : q ≠ 0
⊢ degree 0 ≤ (0 * q).degree

pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q = leadingCoeff D q

Tactic:
hp,

Goal state after:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ 1 * leadingCoeff D q = leadingCoeff D q
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ (map f p).degree = ⊥

Tactic:
hp,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ degree 0 = ⊥
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support

Tactic:
by
  simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

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
⊢ ↑y.support ⊆ Set.range ⇑f

Tactic:
trans ↑(y + w).support

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

α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑(y + w).support ⊆ Set.range ⇑f
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
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ (aeval (f x)) p + (aeval (f x)) q = f ((aeval x) (p + q))

Tactic:
hp,

Goal state after:
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
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ f ((aeval x) p) + (aeval (f x)) q = f ((aeval x) (p + q))
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h✝ : ∃ a_1, a a_1 ≠ b a_1
i : ι := wf.min {i | a i ≠ b i} h✝
j : ι
hr : r j i
h : ¬a j = b j
⊢ j ∈ {i | a i ≠ b i}

Tactic:
by grind

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (f - g).support ⊆ f.support

Tactic:
by
  simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

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)

pp: case add
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
⊢ ∀ (p q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)

pp: case mul_X
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
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)

Tactic:
· simp

Goal state after:
case add
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
⊢ ∀ (p q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)

case mul_X
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
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)
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)
⊢ k (eval₂ f g p) + k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) p) + eval₂ k (⇑k ∘ g) ((map f) q)

Tactic:
hp,

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

Goal state before:
pp: case h
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 : σ →₀ ℕ
⊢ coeff i φ = coeff i (MvPolynomial.C r * ψ)

Tactic:
simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']

Goal state after:
case h
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 : σ →₀ ℕ
⊢ coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 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)
⊢ k (eval₂ f g p) * k (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) p) * eval₂ k (⇑k ∘ g) (X s)

Tactic:
hp,

Goal state after:
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 (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) p) * eval₂ k (⇑k ∘ g) (X s)
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)

pp: case hX
σ : 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 : τ
n : σ →₀ ℕ
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

Tactic:
· simp

Goal state after:
case hX
σ : 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 : τ
n : σ →₀ ℕ
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))
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)
⊢ (map f) (eval₂ C g p) + (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
hp,

Goal state after:
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) + (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
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)
⊢ (map f) (eval₂ C g p) * (map f) (eval₂ C g (X s)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X s))

Tactic:
hp,

Goal state after:
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) (eval₂ C g (X s)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X s))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ ((rename f) p).degrees = Multiset.map f p.degrees

Tactic:
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ p.support.sup ((fun s ↦ toMultiset s) ∘ Finsupp.mapDomain f) = p.support.sup (Multiset.map f ∘ ⇑toMultiset)
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
⊢ ↑((map f) p).coeffs ⊆ ⇑f '' ↑p.coeffs

Tactic:
exact mod_cast coeffs_map f p

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Tactic:
simp_rw [degreeOf_eq_sup]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ ((f + g).support.sup fun m ↦ m n) ≤ max (f.support.sup fun m ↦ m n) (g.support.sup fun m ↦ m n)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ s i ≤ degreeOf i p

Tactic:
exact le_degreeOf_of_mem_support i h

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
⊢ degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j ↦ degreeOf i (f j)

Tactic:
simp_rw [degreeOf_eq_sup]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ j ∈ s, f j).support.sup fun m ↦ m i) ≤ s.sup fun j ↦ (f j).support.sup fun m ↦ m i
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
⊢ degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)

Tactic:
simp_rw [degreeOf_eq_sup]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∏ j ∈ s, f j).support.sup fun m ↦ m i) ≤ ∑ x ∈ s, (f x).support.sup fun m ↦ m i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
⊢ f ≠ 0

Tactic:
by_contra ha

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
ha : f = 0
⊢ False