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

Tactic:
simp

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

Goal state before:
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:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
d : M × M
inst✝ : AddCommMonoid M
⊢ ∑ a, (finTwoArrowEquiv M).symm d a = d.1 + d.2

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 : σ ≃ τ
p : MvPolynomial σ R
⊢ p.totalDegree ≤ ((rename ⇑f.symm) ((rename ⇑f) p)).totalDegree

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
⊢ 0 ∈ {p | p.degrees ≤ s}

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ 1 ≤ degreesLE R σ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
⊢ degreesLE R σ (0 • s) = degreesLE R σ s ^ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑n * ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
simp

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
⊢ coeff 0 (natTrailingDegree 0) = 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ 0).coeff (0 * n) = p.coeff n ^ 0

Tactic:
simp

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

Goal state before:
pp: case empty
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
h : {i | i ∈ ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
⊢ (∅.sum f).degree = ∅.sup fun i ↦ (f i).degree

Tactic:
simp

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

Goal state before:
pp: case insert.inr.inl.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
IH : (∅.sum f).degree = ∅.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (∅.sum f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (∅.sup fun i ↦ (f i).degree)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)

Tactic:
simp

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

Goal state before:
pp: N : ℕ
⊢ (revAt N) 0 = N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
⊢ ((monomial i) r).eraseLead = 0

Tactic:
by
  classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
p : R[X]
n✝ : ℕ
⊢ (reflect N (reflect N p)).coeff n✝ = p.coeff n✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n n✝ : ℕ
⊢ (reflect n (map f p)).coeff n✝ = (map f (reflect n p)).coeff n✝

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
· right
    rw [← C_mul_X_pow_eq_self h]
    simp

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).eraseLead.coeff ((C a).natDegree - 1) = 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
a : R
hnext : (C a).nextCoeff = 0
⊢ (C a).eraseLead = 0

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X + C 0).eraseLead = 0

Tactic:
simp

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

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) (C a))) = coeff m✝ (C a)

Tactic:
eval₂_C,

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (Polynomial.eval₂ C (X default) (Polynomial.C a)) = coeff m✝ (C a)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X default = X i

Tactic:
← Unique.eq_default i

Goal state after:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X i = X i
Module: Mathlib.Algebra.MvPolynomial.Equiv

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p + Polynomial.eval₂ C (X default) q) =
    p + q

Tactic:
MvPolynomial.eval₂_add,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) +
      eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) =
    p + q
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False

Tactic:
simp only [inj (p.coeff 0) hz, map_zero] at A

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (C n) * eval₂ Polynomial.C (fun x ↦ Polynomial.X) (X default ^ (p + 1)) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
eval₂_C,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ Polynomial.C n * eval₂ Polynomial.C (fun x ↦ Polynomial.X) (X default ^ (p + 1)) =
    Polynomial.C n * Polynomial.X ^ (p + 1)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ φ r * a default ^ (Finsupp.single default (d default)) default = φ r * a default ^ d default

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ eval₂ φ a ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f

Tactic:
rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm]

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) ((uniqueAlgEquiv R σ).symm f)) = Polynomial.eval₂ φ (a default) f
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((isEmptyRingEquiv R σ).symm.toRingHom x✝) = coeff m✝ (C x✝)

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : p.natDegree = 0
⊢ 0 = f 0

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : ¬p.natDegree = 0
⊢ (map f p).coeff (p.natDegree - 1) = f (p.coeff (p.natDegree - 1))

Tactic:
simp

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : q.natDegree < n
⊢ (p - q).coeff n = p.coeff n

Tactic:
rw [← natDegree_neg] at dg
  rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f.eraseLead * g) + reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g

Tactic:
hcf,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect N f.eraseLead * reflect O g + reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g

case neg.Cf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

case neg.Nf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i✝)))

Tactic:
simp

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i✝)))

Tactic:
simp

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

Goal state before:
pp: case refine_2.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0

Tactic:
simp

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

Goal state before:
pp: case refine_2.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

Tactic:
simp

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

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none))).comp
        CAlgHom)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]).comp CAlgHom) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none)))
          Polynomial.X).coeff
      n✝ =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]) Polynomial.X).coeff n✝

Tactic:
simp

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

Goal state before:
pp: case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

Tactic:
simp

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

Goal state before:
pp: case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p.comp^[0] q).natDegree = p.natDegree ^ 0 * q.natDegree

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
⊢ (p * C a).nextCoeff = p.nextCoeff * a

Tactic:
by
  by_cases h₀ : a = 0 <;> simp [h₀, nextCoeff, natDegree_mul_C]

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

Goal state before:
pp: case h_zero
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁), (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N 0) * x ^ N = eval₂ i x 0

Tactic:
simp

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ ¬#f.support = 0

Tactic:
hf

Goal state after:
case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ ¬0 + 1 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * ⅟x ^ (N - n) * x ^ (N - n) * x ^ n = i r * x ^ n

Tactic:
mul_assoc (i r),

Goal state after:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * (⅟x ^ (N - n) * x ^ (N - n)) * x ^ n = i r * x ^ n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ (∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i) →
    ∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff i) = 0

Tactic:
rintro ⟨m, h, rfl⟩

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : Option σ →₀ ℕ
h : ¬coeff m.some (((optionEquivLeft R σ) p).coeff (m none)) = 0
⊢ ∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff (m none)) = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ ¬#f.support = 0

Tactic:
hf

Goal state after:
case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ ¬n✝ + 1 + 1 = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 ≤ p.totalDegree

Tactic:
simp

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

Goal state before:
pp: case e_m
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ d = (optionElim m d).some

Tactic:
simp

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

Goal state before:
pp: case e_a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ m = (optionElim m d) none

Tactic:
simp

Goal state after: