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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ a,
    ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
      (revAt (p.natDegree + p.natTrailingDegree)) a = n

Tactic:
use revAt (p.natDegree + p.natTrailingDegree) n

Goal state after:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ (_ : (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)) (_ :
    p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree)) ((revAt (p.natDegree + p.natTrailingDegree)) n) = n
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    q %ₘ g * g ^ n + q /ₘ g * (g * g ^ n) + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc

Tactic:
← mul_assoc,

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    q %ₘ g * g ^ n + q /ₘ g * g * g ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : r₁ * g ^ n + (q₁ * (g * g ^ n) + ∑ x, rs₁ x * g ^ ↑x) = r₂ * g ^ n + (q₂ * (g * g ^ n) + ∑ x, rs₂ x * g ^ ↑x)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
← mul_assoc,

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : r₁ * g ^ n + (q₁ * g * g ^ n + ∑ x, rs₁ x * g ^ ↑x) = r₂ * g ^ n + (q₂ * (g * g ^ n) + ∑ x, rs₂ x * g ^ ↑x)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : r₁ * g ^ n + (q₁ * g * g ^ n + ∑ x, rs₁ x * g ^ ↑x) = r₂ * g ^ n + (q₂ * (g * g ^ n) + ∑ x, rs₂ x * g ^ ↑x)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
← mul_assoc,

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : r₁ * g ^ n + (q₁ * g * g ^ n + ∑ x, rs₁ x * g ^ ↑x) = r₂ * g ^ n + (q₂ * g * g ^ n + ∑ x, rs₂ x * g ^ ↑x)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
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
n : ℕ
⊢ (p * (X ^ n * X ^ 1)).smeval x = p.smeval x * x ^ (n + 1)

Tactic:
← mul_assoc,

Goal state after:
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
n : ℕ
⊢ (p * X ^ n * X ^ 1).smeval x = p.smeval x * x ^ (n + 1)
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:
by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a =>
    simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]

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

Goal state before:
pp: case monomial.succ
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
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)

Tactic:
← mul_assoc,

Goal state after:
case monomial.succ
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
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (0 + 0 + if n = n then w else 0) = w

Tactic:
if_pos rfl,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ 0 + 0 + w = w
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ ((0 + if m = m then v else 0) + if m = n then w else 0) = v

Tactic:
if_pos rfl,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (0 + v + if m = n then w else 0) = v
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (((if k = k then u else 0) + if k = m then v else 0) + if k = n then w else 0) = u

Tactic:
if_pos rfl,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ ((u + if k = m then v else 0) + if k = n then w else 0) = u
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 * (g i * ∏ x ∈ s, g x) +
        (q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i * ∏ k ∈ s, g k +
      ((∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
        ∑ 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:
← mul_assoc,

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 * g i * ∏ x ∈ s, g x +
        (q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i * ∏ k ∈ s, g k +
      ((∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
        ∑ 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.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
j : ι
hj : j ∈ s
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * (g j * ∏ x ∈ s.erase j, g x) +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * (g j * ∏ x ∈ s.erase j, g x)) +
        r j * a j %ₘ g j * (g i * ∏ x ∈ s.erase j, g x))

Tactic:
← mul_assoc,

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
j : ι
hj : j ∈ s
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * g j * ∏ k ∈ s.erase j, g k +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j * ∏ k ∈ s.erase j, g k +
        r j * a j %ₘ g j * g i * ∏ k ∈ s.erase j, 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
⊢ ↑(q + k)! * (aeval r) p' = ↑q ! * (↑((q + k).descFactorial k) * (aeval r) p')

Tactic:
← mul_assoc,

Goal state after:
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
⊢ ↑(q + k)! * (aeval r) p' = ↑q ! * ↑((q + k).descFactorial k) * (aeval r) p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - (X * (monomial P.natDegree) P.leadingCoeff - C η * (monomial P.natDegree) P.leadingCoeff) -
      (monomial P.natDegree) P.nextCoeff

Tactic:
X_mul_monomial,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - ((monomial (P.natDegree + 1)) P.leadingCoeff - C η * (monomial P.natDegree) P.leadingCoeff) -
      (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i * ((q₁ - q₂) * ∏ x ∈ s, g x) +
      g i * (∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x - ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
← mul_assoc,

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i * (q₁ - q₂) * ∏ x ∈ s, g x + g i * (∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x - ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * (↑z * ↑x) + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror

Tactic:
← mul_assoc,

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * ↑z * ↑x + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
rw [List.destutter'_cons]

Goal state after:
case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (if 1 ≠ SignType.sign c₀ then
        1 ::
          List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
            (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))
      else
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : CommRing R
inst✝ : CharZero R
m n : ℕ
⊢ ↑m = ↑n → m = n

Tactic:
simp [QuadraticAlgebra.ext_iff]

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
⊢ w * (z * star z) = 0

Tactic:
← mul_assoc,

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
⊢ w * z * star z = 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) *
      ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
map_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ ((algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i) +
        (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)) *
      ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y z : Rᵐᵒᵖ},
    op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
intro x y z

Goal state after:
R : Type u_1
inst✝ : Rack R
x y z : Rᵐᵒᵖ
⊢ op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
left_cancel

Goal state after:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ z = z ↔ x ◃ z = z
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x y z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)

Tactic:
intro x y z

Goal state after:
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y z : Conj G
⊢ (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
intro x y z

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev =
    gi i ^ (↑j + 1) * (gi i ^ ↑j.rev * (algebraMap R[X] K) (g i) ^ ↑j.rev)

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev = gi i ^ (↑j + 1) * gi i ^ ↑j.rev * (algebraMap R[X] K) (g i) ^ ↑j.rev