mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ stabilizer G ↑s = s.unop

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.unop
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ stdPart x = sSup {r | f r < x}

Tactic:
rw [← neg_inj, ← stdPart_neg, stdPart_eq_sInf f, ← Real.sInf_neg]
  congr 1
  ext
  simp [neg_lt]

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ ∃ y, ((↑f).supSpanSingleton x (f.eval x) hx).toFun y = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))

Tactic:
refine ⟨⟨x, by simpa using Submodule.mem_sup_right (Submodule.mem_span_singleton_self x)⟩, ?_⟩
    apply_fun ofLex
    rw [ofLex_toLex, LinearPMap.toFun_eq_coe, LinearPMap.supSpanSingleton_apply_self]
    ext d
    obtain hdc | hdc := lt_or_ge d c
    · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc]
    rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc, eval, ofLex_toLex]
    apply f.evalCoeff_eq_zero
    contrapose h
    obtain ⟨y, hy⟩ := h
    exact ⟨y, Set.mem_of_mem_of_subset hy (by simpa using (ball_strictAnti K).antitone hdc)⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
⊢ (List.map P.coeff (List.range P.degree.succ)).reverse[k + 1]? =
    (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))[k + 1]?

Tactic:
rw [List.getElem?_eq_none]
      <;> simp

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
⊢ n + P.eraseLead.degree.succ ≤ k

case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
⊢ P.degree.succ ≤ k + 1
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| some (P.coeff (P.degree.succ - 1 - (k + 1)))

Tactic:
arg 1

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| P.coeff (P.degree.succ - 1 - (k + 1))
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p * q)) =
    p • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm p)

Tactic:
induction p using Polynomial.induction_on' with

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p : A[X]
⊢ d' ((aeval x) p) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (aeval x) (derivative p) • d' x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
p : R[X][Y]
⊢ (aevalAeval x y) (swap p) = (aevalAeval y x) p

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
p : R[X][Y]
⊢ (aeval (C x)) p = (mapAlgHom (aeval x)) (swap p)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case monomial
R : Type u_2
inst✝ : CommRing R
n : ℕ
p : R[X]
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) p)) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) p)))

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : R[X][Y]
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) p) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p))

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) p)) = (equivMvPolynomial R) (derivative ((monomial n) p))

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X][Y]
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (derivative p)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ ((monomial n) a).mirror = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)

Tactic:
mul_comm h,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ((ofFn n) v).natDegree < n

Tactic:
rw [Nat.lt_iff_le_pred h, natDegree_le_iff_coeff_eq_zero]
  exact fun _ h ↦ ofFn_coeff_eq_zero_of_ge _ <| Nat.le_of_pred_lt h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
m : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m (p.homogenize n) = if m 0 + m 1 = n then p.coeff (m 0) else 0

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
· simp +contextual

Goal state after:
case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n

Tactic:
by
  apply homogenize_eq_of_isHomogeneous
  · apply_rules [MvPolynomial.IsHomogeneous.mul, isHomogeneous_homogenize]
  · simp [*]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (a :: l)

Tactic:
by
    rw [← h]
    exact l.isChain_destutter' R a

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
⊢ (r • p).smeval x = r • p.smeval x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
⊢ (C r * p).smeval x = r • p.smeval x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ↑a * ↑n ^ n✝ = ↑a * ↑(n ^ n✝)

Tactic:
Nat.cast_npow

Goal state after:
case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ↑a * ↑n ^ n✝ = ↑a * ↑n ^ n✝
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
⊢ p.smeval 0 = p.coeff 0 • 1

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
⊢ (X * p).smeval x = x * p.smeval x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n : ℕ
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ ((monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
⊢ (p * X).smeval x = p.smeval x * x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
m n : ℕ
⊢ p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p * q).smeval x = p.smeval x * q.smeval x

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p.comp q).smeval x = p.smeval (q.smeval x)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
⊢ Commute (p.smeval x) y

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
⊢ Commute (p.smeval x) (q.smeval y)

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
      (Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i *
          ∏ k ∈ (Finset.cons i s hi).erase i, g k +
        ∑ x ∈ s,
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)

Tactic:
Function.update_self,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
      ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i * ∏ k ∈ (Finset.cons i s hi).erase i, g k +
        ∑ x ∈ s,
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) (↑((q + k).descFactorial k) * p')

Tactic:
simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

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

Goal state before:
pp: case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (SignType.sign P.leadingCoeff ::
              (List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0) ++
                List.map (⇑SignType.sign) (c :: cs))))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
            (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (c :: cs)))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
simp only [List.filter_append, List.filter_replicate, List.map_cons, List.filter, ne_eq, hsl]

Goal state after:
case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (match decide ¬False with
          | true =>
            SignType.sign P.leadingCoeff ::
              ((if (decide ¬SignType.sign 0 = 0) = true then
                  List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
                else []) ++
                match decide ¬SignType.sign c = 0 with
                | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
                | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))
          | false =>
            (if (decide ¬SignType.sign 0 = 0) = true then
                List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
              else []) ++
              match decide ¬SignType.sign c = 0 with
              | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
              | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (match decide ¬SignType.sign c = 0 with
            | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
            | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (AddMonoidAlgebra.single (k + k) (↑u * ↑w) + AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v) +
                    AddMonoidAlgebra.single (k + n) (↑u * ↑u) +
                  (AddMonoidAlgebra.single (m + k) (↑v * ↑w) + AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v) +
                    AddMonoidAlgebra.single (m + n) (↑v * ↑u)) +
                (AddMonoidAlgebra.single (n + k) (↑w * ↑w) + AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v) +
                  AddMonoidAlgebra.single (n + n) (↑w * ↑u))).coeff) }

Tactic:
AddMonoidAlgebra.coeff_add,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((AddMonoidAlgebra.single (k + k) (↑u * ↑w)).coeff +
                    (AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v)).coeff +
                  (AddMonoidAlgebra.single (k + n) (↑u * ↑u)).coeff +
                ((AddMonoidAlgebra.single (m + k) (↑v * ↑w)).coeff +
                    (AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v)).coeff +
                  (AddMonoidAlgebra.single (m + n) (↑v * ↑u)).coeff) +
              ((AddMonoidAlgebra.single (n + k) (↑w * ↑w)).coeff +
                  (AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v)).coeff +
                (AddMonoidAlgebra.single (n + n) (↑w * ↑u)).coeff))) }
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations

Tactic:
· simp [hpz]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

Tactic:
· simp [hpz]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1