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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map (⇑(lcoeff R n) ∘ f) l).sum = (List.map (fun a ↦ (f a).coeff n) l).sum

Tactic:
Function.comp_def,

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map (fun x ↦ (lcoeff R n) (f x)) l).sum = (List.map (fun a ↦ (f a).coeff n) l).sum
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ g₀ self_mem_Iic g₀

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ g₀ self_mem_Iic g₀

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i

Tactic:
· rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]

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

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

Tactic:
Finsupp.notMem_support_iff.mp h,

Goal state after:
case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : ap ∉ p.coeff.support
a : A
x✝¹ : a ∈ q.coeff.support
x✝ : ap + a = ap + aq
⊢ 0 * q.coeff a = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
      rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
    rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]

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

Goal state before:
pp: case hmem
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).coeff.support

pp: case hmax
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

Tactic:
· simp_rw [Finsupp.mem_support_iff, coeff_supDegree_add_supDegree hD hadd]
    exact hpq

Goal state after:
case hmax
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ (X - C c).nextCoeff = -c

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = Subalgebra.map (aeval x) ⊤

Tactic:
← adjoin_X,

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = Subalgebra.map (aeval x) R[ X]
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (C (f.coeff 0))

Tactic:
refine IsUnit.map C ?_

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (f.coeff 0)
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
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u - single i 1 + single i 1 = u

Tactic:
sub_single_one_add h,

Goal state after:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u + single i 1 - single i 1 = u
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 ≠ b
⊢ False

Tactic:
rw [Function.ne_iff] at h

Goal state after:
ι : 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
⊢ False
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : f wit < g wit
⊢ P (toLex f) (toLex g)

pp: case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : g wit < f wit
⊢ P (toLex f) (toLex g)

Tactic:
· exact h_lt ⟨wit, fun j hj ↦ notMem_neLocus.mp (Finset.notMem_of_lt_min hj h), hwit⟩

Goal state after:
case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : g wit < f wit
⊢ P (toLex f) (toLex g)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
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
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
rw [Submodule.mul_le]

Goal state after:
case refine_2
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 ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).vars = s.support

Tactic:
rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ ((rename f) ((killCompl hf) p)).support ⊆ p.support

Tactic:
classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..

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

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

Tactic:
simp only [degreeOf]
  convert! Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]

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
⊢ 0 i = 0

Tactic:
by simp only [coe_zero, Pi.zero_apply]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1, f i_1 ((cons i σ) i_1) = f 0 i + ∑ i, Fin.tail f i (σ i)

Tactic:
simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 i + ∑ i, f i.succ (σ i) = f 0 i + ∑ i, Fin.tail f i (σ i)
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
d : M × M
inst✝ : AddCommMonoid M
⊢ (((finTwoArrowEquiv' M).symm d).sum fun x n ↦ n) = d.1 + d.2

Tactic:
apply (Finsupp.equivFunOnFinite_symm_sum _).trans
  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
⊢ ↑(C (p.coeff n)).natDegree + n • q.degree ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree

Tactic:
grw [degree_le_natDegree]

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

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

Tactic:
rw [C_mul_X_pow_eq_monomial]
  exact le_trailingDegree_monomial

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
coeff_eq_zero_of_lt_natTrailingDegree hi,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ 0 * q.coeff (i, j).2 = 0
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:
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.EraseLead

Goal state before:
pp: case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
· rw [he, mul_zero]
    by_cases he₂ : ((X - C x) * P).eraseLead = 0
    · simp [he₂]
    suffices #((X - C x) * P).support ≤ 2 by
      rw [← card_support_eq_zero]
      linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]
    have h₂ : #(X - C x).support = 2 := by
      simpa [← sub_eq_add_neg] using!
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)
    have hmul := card_support_mul_le (p := X - C x) (q := P)
    rw [h₂] at hmul
    linarith [card_support_le_one_of_eraseLead_eq_zero he]

Goal state after:
case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
by_cases q0 : q.natDegree = 0
  · rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
  · by_cases p0 : p = 0
    · simp only [p0, zero_comp, natDegree_zero, zero_mul]
    · simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ p.degree + (C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
← degree_mul,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ n • p.nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff

Tactic:
succ_nsmul

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ n • p.nextCoeff + p.nextCoeff = n • p.nextCoeff + p.nextCoeff
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ reflect (-f).natDegree (-f) = -reflect f.natDegree f

Tactic:
reflect_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ -reflect (-f).natDegree f = -reflect f.natDegree f
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse

Tactic:
by
  rw [reverse, reverse, reflect_neg, natDegree_neg]

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ↑p.natDegree ∈ List.map natDegree l

Tactic:
rw [List.mem_map]

Goal state after:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ∃ a ∈ l, a.natDegree = ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
⊢ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
⊢ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ (Multiset.map (Nat.cast ∘ natDegree) t).sum = (Multiset.map degree t).sum

Tactic:
Function.comp_def,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ (Multiset.map (fun x ↦ ↑x.natDegree) t).sum = (Multiset.map degree t).sum
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ toMvPolynomial i = (MvPolynomial.rename fun x ↦ i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : σ → S
i : σ
⊢ (aeval f).comp (toMvPolynomial i) = Polynomial.aeval (f i)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : CommSemiring R
f : σ → τ
a : σ
⊢ (rename f).comp (toMvPolynomial a) = toMvPolynomial (f a)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree = p.degree

Tactic:
refine le_antisymm ?_ ?_
  · rw [degree_le_iff_coeff_zero]
    intro m hm
    rw [degree_lt_iff_coeff_zero] at hm
    simp [hm m le_rfl]
  · rw [degree_le_iff_coeff_zero]
    intro m hm
    rw [degree_lt_iff_coeff_zero] at hm
    refine h ?_
    simpa using hm m le_rfl

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Tactic:
rintro ⟨k, x, hx, rfl⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(C x * X ^ k).support = 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x) → ∃ p ∈ I, p.leadingCoeff = x

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ p ∈ I, p.leadingCoeff = x) → ∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x

Tactic:
· rintro ⟨i, p, hpI, _, rfl⟩
      exact ⟨p, hpI, rfl⟩

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ p ∈ I, p.leadingCoeff = x) → ∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun n ↦ I.leadingCoeffNth n

Tactic:
intro i j

Goal state after:
case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) i) ((fun n ↦ I.leadingCoeffNth n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) j) ((fun n ↦ I.leadingCoeffNth n) z)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) ∈ p

Tactic:
apply subset_span

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := ⋯
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) ∈ {g | ∃ i, g = C (f.coeff i)}
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_unop,

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_unop,

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = f

Tactic:
induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after: