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

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

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∑ v ∈ p.support, (monomial v) (coeff v p)).coeff = p.coeff
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.Rename

Goal state before:
pp: case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q

Tactic:
intro r

Goal state after:
case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ ∃ s q, C r = (rename Subtype.val) q
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.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₁
p : MvPolynomial σ R
⊢ (eval g) ((map f) p) = eval₂ f g p

Tactic:
apply MvPolynomial.induction_on p <;> · simp +contextual

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

Goal state before:
pp: case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d p ≠ 0 ∧ j ∈ d.support

Tactic:
;

Goal state after:
case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d p ≠ 0 ∧ j ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d p ≠ 0

Tactic:
;

Goal state after:
case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d p ≠ 0
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✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
intro r

Goal state after:
case refine_1
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
⊢ r ∈ M * N → ∀ (i : σ →₀ ℕ), (monomial i) r ∈ coeffsIn σ M * coeffsIn σ N
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support

Tactic:
;

Goal state after:
case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0

Tactic:
;

Goal state after:
case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), f (coeff m (ofCoeff (mapRange g hg φ.coeff))) = coeff m φ) ↔
    ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), f (coeff m (ofCoeff (mapRange g hg φ.coeff))) = coeff m φ) ↔
    ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
;

Goal state after:
case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.vars = p.degrees.toFinset

Tactic:
vars

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset
Module: Mathlib.Algebra.MvPolynomial.Variables

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

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ (C (coeff 0 p)).vars = ∅
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees
Module: Mathlib.Algebra.MvPolynomial.CommRing

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

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
a✝ : σ →₀ ℕ
⊢ a✝ ∈ (-p).support ↔ a✝ ∈ p.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
;

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.degrees

Tactic:
;

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.degrees
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
ha : f = 0
⊢ False

Tactic:
;

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

Goal state before:
pp: case a.add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp : (aeval f) p ∈ Algebra.adjoin R (range f)
hq : (aeval f) q ∈ Algebra.adjoin R (range f)
⊢ (aeval f) p + (aeval f) q ∈ Algebra.adjoin R (range f)

Tactic:
;

Goal state after:
case a.add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp : (aeval f) p ∈ Algebra.adjoin R (range f)
hq : (aeval f) q ∈ Algebra.adjoin R (range f)
⊢ (aeval f) p + (aeval f) q ∈ Algebra.adjoin R (range f)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree 0 = p.totalDegree

Tactic:
Nat.max_zero

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ p.totalDegree = p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ (Finsupp.single i e).support = {i}

Tactic:
Finsupp.support_single _ he

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ {i} = {i}
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
a✝ : Fin n
⊢ (t.update i.succ y).tail a✝ = (t.tail.update i y) a✝

Tactic:
;

Goal state after:
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
a✝ : Fin n
⊢ (t.update i.succ y).tail a✝ = (t.tail.update i y) a✝
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ (cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
by
  intro i hi
  suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa
  apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)
  rintro i rfl
  simpa [Finsupp.mem_support_iff] using hi

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1, (cons i σ) i_1 = i + σ.sum fun x e ↦ e

Tactic:
sum_fintype _ _ (fun _ => rfl)

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1, (cons i σ) i_1 = i + ∑ i, σ i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (fun s ↦ s.sum fun x e ↦ e) = fun m ↦ (toMultiset m).card

Tactic:
;

Goal state after:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (fun s ↦ s.sum fun x e ↦ e) = fun m ↦ (toMultiset m).card
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0

Tactic:
;

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0

Tactic:
;

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, m i

Tactic:
;

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, m i
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((algebraMap R (MvPolynomial σ S)) x✝) =
    coeff m✝ (((algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))) x✝)

Tactic:
;

Goal state after:
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((algebraMap R (MvPolynomial σ S)) x✝) =
    coeff m✝ (((algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))) x✝)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ (aeval fun i ↦ if i ∈ s then X i else 0) (∑ v ∈ q.support, (monomial v) (coeff v q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)

Tactic:
MvPolynomial.aeval_sum

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ ∑ i ∈ q.support, (aeval fun i ↦ if i ∈ s then X i else 0) ((monomial i) (coeff i q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree) p.leadingCoeff = p

Tactic:
by
  classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]

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
⊢ 0 ≤ p.natDegree * q.natDegree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := ⋯
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Tactic:
;

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := ⋯
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = (p + q).coeff m

Tactic:
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree

Tactic:
;

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ nextCoeffUp 0 = 0

Tactic:
by simp [nextCoeffUp]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

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

Goal state before:
pp: case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := toFinsupp✝ }).support = image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Tactic:
;

Goal state after:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := toFinsupp✝ }).support = image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
a✝ : ℕ
⊢ a✝ ∈ (reflect N { toFinsupp := toFinsupp✝ }).support ↔ a✝ ∈ image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Tactic:
;

Goal state after:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
a✝ : ℕ
⊢ a✝ ∈ (reflect N { toFinsupp := toFinsupp✝ }).support ↔ a✝ ∈ image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support
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:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
N : ℕ
p : R[X]
n✝ : ℕ
⊢ (reflect N (reflect N p)).coeff n✝ = p.coeff n✝
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:
;

Goal state after:
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✝
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
rcases eq_or_ne (natDegree p) 0 with h | h

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
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:
;

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r)

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₁
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((monomial (Finsupp.single (Sum.inl s) 1)) 1) =
    (monomial (Finsupp.single s 1)) 1

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₁
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((monomial (Finsupp.single (Sum.inl s) 1)) 1) =
    (monomial (Finsupp.single s 1)) 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₂
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((monomial (Finsupp.single (Sum.inr s) 1)) 1) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((monomial (Finsupp.single s 1)) 1)

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₂
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((monomial (Finsupp.single (Sum.inr s) 1)) 1) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((monomial (Finsupp.single s 1)) 1)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (C r))) = coeff m✝ (coeff m✝¹ (C (C r)))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (C r))) = coeff m✝ (coeff m✝¹ (C (C r)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (C r))) = coeff m✝ (C r)

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (C r))) = coeff m✝ (C r)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inl c)))) = coeff m✝ (coeff m✝¹ (X c))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inl c)))) = coeff m✝ (coeff m✝¹ (X c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (X c)) = coeff m✝ (X (Sum.inl c))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (X c)) = coeff m✝ (X (Sum.inl c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inr c)))) = coeff m✝ (coeff m✝¹ (C (X c)))

Tactic:
;

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inr c)))) = coeff m✝ (coeff m✝¹ (C (X c)))