mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 1 ∈ coeffsIn σ M ↔ 1 ∈ M

Tactic:
simpa using

Goal state after:
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
⊢ 1 ∈ coeffsIn σ M ↔ 1 ∈ M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mp
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_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
j : σ →₀ ℕ
⊢ coeff j p ∈ M

Tactic:
simpa using

Goal state after:
case mp
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_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
j : σ →₀ ℕ
⊢ coeff j p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mp
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 : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M

pp: case mpr
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 : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M

Tactic:
· rintro hp j
    simpa using hp (j + i)

Goal state after:
case mpr
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 : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
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₁
h : Injective ⇑(map f)
r r' : R
eq : f r = f r'
⊢ r = r'

Tactic:
simpa using

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
h : Injective ⇑(map f)
r r' : R
eq : f r = f r'
⊢ r = r'
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₁
h✝ : Surjective ⇑(map f)
s : S₁
p : MvPolynomial σ R
h : (map f) p = C s
⊢ f (coeff 0 p) = s

Tactic:
simpa using

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
h✝ : Surjective ⇑(map f)
s : S₁
p : MvPolynomial σ R
h : (map f) p = C s
⊢ f (coeff 0 p) = s
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
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p = 0

Tactic:
simpa using

Goal state after:
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
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1.add
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 : σ →₀ ℕ
x : S
hx✝ : x ∈ M * N
y : S
hy✝ : y ∈ M * N
hx : (monomial s) x ∈ coeffsIn σ M * coeffsIn σ N
hy : (monomial s) y ∈ coeffsIn σ M * coeffsIn σ N
⊢ (monomial s) (x + y) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
simpa using

Goal state after:
case refine_1.add
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 : σ →₀ ℕ
x : S
hx✝ : x ∈ M * N
y : S
hy✝ : y ∈ M * N
hx : (monomial s) x ∈ coeffsIn σ M * coeffsIn σ N
hy : (monomial s) y ∈ coeffsIn σ M * coeffsIn σ N
⊢ (monomial s) x + (monomial s) y ∈ coeffsIn σ M * coeffsIn σ N
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ q.degrees ≤ (p + q).degrees

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ q.degrees ≤ (p + q).degrees
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✝ : Algebra R S
M : Submodule R S
⊢ coeffsIn σ M ^ 0 ≤ coeffsIn σ (M ^ 0)

Tactic:
simpa using

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ ∃ y, (algebraMap R S) y = 1
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p + -q) ≤ max (degreeOf i p) (degreeOf i q)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x ∈ f.support ∧ x j + 1 ≤ ((fun m ↦ m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x

Tactic:
simpa using

Goal state after:
case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ ¬coeff x f = 0
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬s i = 0 ∧ i.succ = i.succ

Tactic:
simpa using

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬s i = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = s i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
⊢ ¬coeff s p + coeff s q = 0

Tactic:
rwa [this, add_zero]

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
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : R
hs : ∀ (i : σ →₀ ℕ), f (coeff i (C a)) ∈ s
⊢ eval₂ f v (C a) ∈ s

Tactic:
simpa using

Goal state after:
case C
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : R
hs : ∀ (i : σ →₀ ℕ), f (coeff i (C a)) ∈ s
⊢ f a ∈ s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial_add.refine_1
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ b ∈ s

Tactic:
simpa using

Goal state after:
case monomial_add.refine_1
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ b ∈ s
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 σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ ((algebraMap R (MvPolynomial σ R)) c).degrees + x.degrees ≤ s

Tactic:
simpa using

Goal state after:
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 σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ x.degrees ≤ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ toMultiset a ≤ s

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ toMultiset i ≤ s + t
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j
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)
u : σ →₀ ℕ
hu : u ∈ q.support
i : σ
hi : i ∈ u.support
⊢ (if i ∈ s then X i else 0) ^ u i = X i ^ u i

Tactic:
by simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ?m.25

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ?m.25
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n ≤ (X ^ n).trailingDegree

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n ≤ (X ^ n).trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ (C a * f).natDegree ≤ f.natDegree

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ (C a * f).natDegree ≤ f.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
a : R
⊢ (f * C a).natDegree ≤ f.natDegree

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
a : R
⊢ (f * C a).natDegree ≤ f.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ p.coeff p.natTrailingDegree = 0

Tactic:
← coeff_mul_X_pow

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ (p * X ^ ?a.n✝).coeff (p.natTrailingDegree + ?a.n✝) = 0

case a.n
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ ℕ
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
simpa using

Goal state after:
case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
simpa using

Goal state after:
case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
H : f y = 0
⊢ (f x).degree ≠ (f y).degree

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
H : f y = 0
⊢ ¬f x = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Tactic:
add_tsub_cancel_left

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)

Tactic:
add_tsub_cancel_left

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)

Tactic:
add_tsub_cancel_left

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + o'
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r * X).eraseLead = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r * X).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = q.coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ reflect 1 X = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ reflect 1 X = 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = p.coeff q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
· rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
    intro x hx
    simp [H x hx]

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

Goal state before:
pp: case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
n : ℕ
P Q : MvPolynomial σ R
hP : ((uniqueAlgEquiv R σ) P).coeff n = coeff (Finsupp.single default n) P
hQ : ((uniqueAlgEquiv R σ) Q).coeff n = coeff (Finsupp.single default n) Q
⊢ ((uniqueAlgEquiv R σ) (P + Q)).coeff n = coeff (Finsupp.single default n) (P + Q)

Tactic:
simpa using

Goal state after:
case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
n : ℕ
P Q : MvPolynomial σ R
hP : ((uniqueAlgEquiv R σ) P).coeff n = coeff (Finsupp.single default n) P
hQ : ((uniqueAlgEquiv R σ) Q).coeff n = coeff (Finsupp.single default n) Q
⊢ (eval₂ Polynomial.C (fun x ↦ Polynomial.X) P).coeff n + (eval₂ Polynomial.C (fun x ↦ Polynomial.X) Q).coeff n =
    coeff (Finsupp.single default n) P + coeff (Finsupp.single default n) Q
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: 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
hf : #f.support = 0
⊢ f = 0

Tactic:
simpa using

Goal state after:
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
hf : #f.support = 0
⊢ f = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
simpa using

Goal state after:
case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ ¬coeff σ (((optionEquivLeft R S₁) p).coeff i) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
rw [totalDegree, Finset.sup_le_iff]

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
· exact add_comm _ _

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
simpa using

Goal state after:
case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ ¬coeff σ (((optionEquivLeft R S₁) p).coeff i) = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) ((revAt f.natDegree) f.natTrailingDegree)) = f.trailingCoeff

Tactic:
revAt_invol,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natTrailingDegree = f.trailingCoeff
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ (((finSuccEquiv R n) f).coeff i).support
⊢ cons i m ∈ f.support

Tactic:
simpa using

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ (((finSuccEquiv R n) f).coeff i).support
⊢ ¬coeff m (((finSuccEquiv R n) f).coeff i) = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max 0 (Multiset.map natDegree ⟦a⟧)

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), a.sum.natDegree ≤ List.foldr max 0 (List.map natDegree a)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
simpa using

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ ¬coeff m (((finSuccEquiv R n) f).coeff i) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : ¬coeff m f = 0
⊢ ¬coeff (cons (m 0) m.tail) f = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : ¬coeff m f = 0
⊢ ¬coeff m f = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ x ∈ ((finSuccEquiv R n) f).support ↔ x ∈ (fun m ↦ m 0) '' ↑f.support

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ ¬((finSuccEquiv R n) f).coeff x = 0 ↔ ∃ x_1, ¬coeff x_1 f = 0 ∧ x_1 0 = x