mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
a : WithTop α
⊢ a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤

Tactic:
simp [untop₀]

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ ⊤.untop₀ = 0

Tactic:
simp [untop₀]

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ untop₀ 0 = 0

Tactic:
simp [untop₀]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk.inl
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : mk x ≤ 0
⊢ ∃ n, mk x ≤ n • mk y

pp: case mk.mk.inr
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : 0 < mk x
⊢ ∃ n, mk x ≤ n • mk y

Tactic:
· use 0
      rwa [zero_nsmul]

Goal state after:
case mk.mk.inr
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : 0 < mk x
⊢ ∃ n, mk x ≤ n • mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ 0 = 0⁻¹

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0

Tactic:
inv_zero

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ 0 = 0

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x / y) = stdPart x / stdPart y

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x * y⁻¹) = stdPart x / stdPart y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x * y⁻¹) = stdPart x / stdPart y

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x * y⁻¹) = stdPart x * (stdPart y)⁻¹
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
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
⊢ P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)

Tactic:
apply List.ext_getElem?

Goal state after:
case neg
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
⊢ ∀ (i : ℕ), P.coeffList[i]? = (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList))[i]?
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
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
⊢ Option.map P.coeff (some (P.degree.succ - 1 - (k + 1))) =
    (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse)[k]?

Tactic:
Option.map_some

Goal state after:
case neg
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))) =
    (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse)[k]?
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
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
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) = Option.map P.eraseLead.coeff (some (P.eraseLead.degree.succ - 1 - (k - n)))

Tactic:
Option.map_some

Goal state after:
case neg
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
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ C p.leadingCoeff * X ^ n + p.eraseLead = X ^ n + p.eraseLead

Tactic:
hp.leadingCoeff_eq,

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ C 1 * X ^ n + p.eraseLead = X ^ n + p.eraseLead
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
hp.leadingCoeff_eq,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ 1 * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
hp.leadingCoeff_eq,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ 1 * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
⊢ (p + q).coeff n = 1

Tactic:
coeff_add_eq_left_of_lt hq

Goal state after:
case inr.refine_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Nontrivial R
⊢ p.coeff n = 1
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + q).IsMonicOfDegree n

Tactic:
by
  rcases subsingleton_or_nontrivial R with H | H
  · simpa using hp
  refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩
  · exact natDegree_add_le_of_degree_le hp.natDegree_eq.le hq.le
  · rw [coeff_add_eq_left_of_lt hq]
    exact ((isMonicOfDegree_iff p n).mp hp).2

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1

Tactic:
hp.leadingCoeff_eq,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ 1 * q.leadingCoeff ^ p.natDegree = 1
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror 0 = mirror 0 * q.mirror

Tactic:
mirror_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ 0 = 0 * q.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror 0 = p.mirror * mirror 0

Tactic:
mirror_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ 0 = p.mirror * 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a l <+ a :: l

Tactic:
induction l generalizing a with

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

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

Tactic:
induction l generalizing a with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))

Tactic:
simp_rw [map_cons, destutter_cons_cons, ← this]

Goal state after:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ((p.homogenize p.natDegree).coeff.sum fun x c ↦ f c) = p.sum fun x c ↦ f c

Tactic:
rw [MvPolynomial.sum_def, sum_def p]
  -- We set up a bijection between the sets indexing the terms on both sides
  -- and show that it maps the terms in the one sum to those in the other.
  refine Finset.sum_nbij' (fun s ↦ s 0) (fun n ↦ fun₀ | 0 => n | 1 => p.natDegree - n)
    (fun s hs ↦ ?_) (fun n hn ↦ ?_) (fun s hs ↦ ?_) (fun n hn ↦ by simp)
    fun s hs ↦ ?_
  · simpa [coeff_homogenize, sum_eq_natDegree_of_mem_support_homogenize p hs] using hs
  · simpa [coeff_homogenize, mem_support_iff.mp hn]
      using Nat.add_sub_of_le <| le_natDegree_of_mem_supp n hn
  · -- speeds up `grind` quite a bit
    grind only [= Finsupp.update_apply, = Finsupp.single_apply,
      sum_eq_natDegree_of_mem_support_homogenize p hs]
  · simp [coeff_homogenize, sum_eq_natDegree_of_mem_support_homogenize p hs]

Goal state after:
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 - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    (X - C η) * (P - (monomial P.natDegree) P.leadingCoeff) - (monomial P.natDegree) P.nextCoeff

Tactic:
mul_sub,

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 - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    (X - C η) * P - (X - C η) * (monomial P.natDegree) P.leadingCoeff - (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ 2 * (trinomial k m n ?m.227 ?m.228 ↑w).natDegree = 2 * n'

pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ ℤ

pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ ℤ

Tactic:
←
      hp,

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ 2 * p.natDegree = 2 * n'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
ih : ∀ m < 0, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
hxcQ : ((X - C η) * P).coeff 1 = P.coeff 0
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (List.filter (fun x ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign) (List.map P.coeff (List.range (P.natDegree + 1)).reverse)))).length -
        1 +
      1 ≤
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.filter (fun x ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign)
              (List.map ((X - C η) * P).coeff (List.range (((X - C η) * P).natDegree + 1)).reverse)))).length -
      1

Tactic:
simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
⊢ s_nC_mul = -1

Tactic:
have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
this : P.coeff d = 0
⊢ s_nC_mul = -1
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₃
⊢ q.i * (c₂ • q.j - q.k) = -c₁ • q.j

Tactic:
mul_sub,

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₃
⊢ q.i * c₂ • q.j - q.i * q.k = -c₁ • q.j
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₃
⊢ q.i * (c₂ • q.j - q.i * q.j) * q.j = -((c₁ * c₃) • 1)

Tactic:
mul_sub,

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₃
⊢ (q.i * c₂ • q.j - q.i * (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
exact h_add

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
exact h_add

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
exact h_add

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.add
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ w✝ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r w✝ x✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) w✝ x✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) (w✝ + y✝) (x✝ + z✝)

Tactic:
exact (RingQuot.ringCon r).add ‹_› ‹_›

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk.mk
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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝¹ } - { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝¹ } + -{ toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg]

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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (n : ℕ) (a : RingQuot r), Int.negSucc n • a = -(↑n.succ • a)

Tactic:
by
    rintro n ⟨⟨⟩⟩
    simp [smul_quot, neg_quot, add_mul]

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
p q : StarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
by obtain ⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ C a * X = (monomial 1) a

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
m : ℕ
⊢ m ∈ ((monomial n) a).support ↔ m ∈ {n}

Tactic:
simp [monomial_def, support_eq_skewMonoidAlgebra_support, h]

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

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

Tactic:
SkewPolynomial.coeff_add

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : AddMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
inhabit G
  refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩
  rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj
  exact single_injective default (ha inj)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.sum g).coeff a₂ = f.sum fun a₁ b ↦ (g a₁ b).coeff a₂

Tactic:
by
  simp_rw [coeff_sum', sum_def, Finsupp.sum_apply]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddGroup k
a : SkewMonoidAlgebra k G
⊢ -a + a = 0

Tactic:
by cases a; simp [← ofCoeff_neg, ← ofCoeff_add]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
⊢ a * b = b * a

Tactic:
by
    have hgk (g : G) (r : k) : g • r = r := by
      rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]
    simp only [mul_def, hgk, sum_def]
    rw [Finsupp.sum_comm]
    exact Finsupp.sum_congr (fun x _ ↦ Finsupp.sum_congr
      (fun y _ ↦ by rw [mul_comm, mul_comm (a.coeff y) _]))

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ kerIdeal R M ^ 2 = ⊥

Tactic:
simp only [pow_two, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]
  rintro x hx y hy
  rw [hx, hy, mem_bot, inr_mul_inr]

Goal state after: