mathlib-initiative/mathlib-tactics huggingface dataset:
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 ^ ↑(Fin.last n) + (q /ₘ g * g ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc)

Tactic:
Fin.val_last,

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 ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
q₁ q₂ : R[X]
r₁ r₂ : Fin 0 → R[X]
hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree
hf : q₁ * g ^ 0 + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ 0 + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂

Tactic:
simpa using hf

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

Goal state before:
pp: case monomial.succ
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
a : R
n : ℕ
⊢ a • (0 ^ n * 0) = 0 • 1

Tactic:
mul_zero,

Goal state after:
case monomial.succ
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
a : R
n : ℕ
⊢ a • 0 = 0 • 1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
mul_zero,

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + 0 + 0)
hy : IsUnit (0 + y + 0)
hz : IsUnit (0 + 0 + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 +
      ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + (trinomial k m n ↑u ↑v ↑w).coeff n ^ 2) =
    3

Tactic:
trinomial_leading_coeff' hkm hmn,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 + ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + ↑w ^ 2) = 3
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 + (monomial (n - m + k + n)) ↑w) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((monomial k) ↑u * ((monomial k) ↑w + (monomial (n - m + k)) ↑v + (monomial n) ↑u) +
                    (monomial m) ↑v * ((monomial k) ↑w + (monomial (n - m + k)) ↑v + (monomial n) ↑u) +
                  (monomial n) ↑w * ((monomial k) ↑w + (monomial (n - m + k)) ↑v + (monomial n) ↑u)).toFinsupp.coeff) }

Tactic:
mul_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))
            ((monomial k) ↑u * (monomial k) ↑w + (monomial k) ↑u * (monomial (n - m + k)) ↑v +
                      (monomial k) ↑u * (monomial n) ↑u +
                    ((monomial m) ↑v * (monomial k) ↑w + (monomial m) ↑v * (monomial (n - m + k)) ↑v +
                      (monomial m) ↑v * (monomial n) ↑u) +
                  ((monomial n) ↑w * (monomial k) ↑w + (monomial n) ↑w * (monomial (n - m + k)) ↑v +
                    (monomial n) ↑w * (monomial n) ↑u)).toFinsupp.coeff) }
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hg : ∀ i ∈ ∅, (g i).Monic
hgg : (↑∅).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i ∈ ∅, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ ∅, (r₂ i).degree < (g i).degree
hf : q₁ * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r₁ i * ∏ k ∈ ∅.erase i, g k = q₂ * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r₂ i * ∏ k ∈ ∅.erase i, g k
⊢ q₁ = q₂ ∧ ∀ i ∈ ∅, r₁ i = r₂ i

Tactic:
simpa using hf

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

Goal state before:
pp: case hq
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * 0
⊢ False

Tactic:
mul_zero,

Goal state after:
case hq
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
hp : map (algebraMap R A) p = 0
⊢ False
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 + (∑ 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_add,

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this : P.natDegree + 2 = ((X - C η) * P).coeffList.length
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have := leadingCoeff_monic_mul (q := P) (monic_X_sub_C η)

Goal state after:
case h.left
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝¹ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝ : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this : ((X - C η) * P).leadingCoeff = P.leadingCoeff
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
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
hgid : g i ∣ r₂ i - r₁ i
hf : g i * 0 = (0 - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
mul_zero,

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
hgid : g i ∣ r₂ i - r₁ i
hf : 0 = (0 - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).re = (x✝² • x✝¹ • x✝).re

Tactic:
simp [mul_smul]

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).im = (x✝² • x✝¹ • x✝).im

Tactic:
simp [mul_smul]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : QuadraticAlgebra R a b →ₐ[R] A
h : f ω = g ω
⊢ f = g

Tactic:
by
  ext ⟨x, y⟩
  simp [mk_eq_add_smul_omega, h]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
η : R
η_root : η ∈ P.roots
η_pos : 0 < η
⊢ n✝ + 1 ≤ P.signVariations

Tactic:
obtain ⟨Q, rfl⟩ := dvd_iff_isRoot.mpr (isRoot_of_mem_roots η_root)

Goal state after:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ n✝ + 1 ≤ ((X - C η) * Q).signVariations
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    x.re • 1 * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k) +
          x.imI • q.i * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k) +
        x.imJ • q.j * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k) +
      x.imK • q.k * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)

Tactic:
mul_add,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    x.re • 1 * y.re • 1 + x.re • 1 * y.imI • q.i + x.re • 1 * y.imJ • q.j + x.re • 1 * y.imK • q.k +
          (x.imI • q.i * y.re • 1 + x.imI • q.i * y.imI • q.i + x.imI • q.i * y.imJ • q.j + x.imI • q.i * y.imK • q.k) +
        (x.imJ • q.j * y.re • 1 + x.imJ • q.j * y.imI • q.i + x.imJ • q.j * y.imJ • q.j + x.imJ • q.j * y.imK • q.k) +
      (x.imK • q.k * y.re • 1 + x.imK • q.k * y.imI • q.i + x.imK • q.k * y.imJ • q.j + x.imK • q.k * y.imK • q.k)
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝

Tactic:
exact congr_arg some (left_distrib _ _ _)

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p f

Tactic:
suffices p (single a (f.coeff a) + f.erase a) by rwa [single_add_erase] at this
    classical
    apply ha
    · rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl
    · simp only [← mem_support_iff, hf, Finset.mem_cons_self]
    · apply ih
      rw [support_erase, hf, Finset.erase_cons]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ↑0 = 0

Tactic:
by simp +instances [instNatCast, natCast, ← zero_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
ringQuotToIdealQuotient,

Goal state after:
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (lift ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 0 = q * 0

Tactic:
mul_zero,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ 0 = q * 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : SkewPolynomial R
n : ℕ
⊢ (-p).coeff n = -p.coeff n

Tactic:
simp [← add_eq_zero_iff_eq_neg, ← coeff_add, neg_add_cancel p]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (0 + unsym x✝ * 0)) = 0

Tactic:
mul_zero,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (0 + 0)) = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * 0) = 0

Tactic:
mul_zero,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym 0 = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * 0 + 0)) = 0

Tactic:
mul_zero,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (0 + 0)) = 0
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i, f i) = sInf ((fun i ↦ untrop (f i)) '' ↑univ)

Tactic:
untrop_sum_eq_sInf_image,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf (untrop ∘ f '' ↑univ) = sInf ((fun i ↦ untrop (f i)) '' ↑univ)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (star (toConv (x • 1 - (star f).ofConv))).ofConv ↔ IsUnit (star x • 1 - f.ofConv)

Tactic:
simp [one_eq_id]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s

Tactic:
let s : ∀ x : ↑(iSup U), T x := fun x => sf (index x) ⟨x.1, index_spec x⟩

Goal state after:
X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
s : (x : ↥(iSup U)) → T ↑x := fun x ↦ sf (index x) ⟨↑x, ⋯⟩
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx : (toPushforwardStalkAlgHom R S p) x = 0
⊢ ∃ m, m • x = 0

Tactic:
rw [toPushforwardStalkAlgHom_apply,
      ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
      toPushforwardStalk] at hx

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap (↑(CommRingCat.of ↑S))
              ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
            ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ j y, (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
by
    simp_rw [presieve₀_mem_precoverage_iff, Set.mem_range]
    grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))).hom ≫ Hom.stalkMap snd p =
    Hom.stalkMap f x ≫ (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)).hom

Tactic:
by
      subst hx
      simp [← Scheme.Hom.stalkMap_comp, ← Scheme.Hom.stalkMap_comp,
        Scheme.Hom.stalkMap_congr_hom _ _ h.w]

Goal state after: