mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ b', b' < b ∧ c < a * b'

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)
  exact ⟨a', ha', div_lt_iff_lt_mul'.1 hc'⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s))

Tactic:
← sum_inter_add_sum_sdiff s r _

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s ∩ r, x + ∑ x ∈ s \ r, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s))
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ (c + ↑(#s) - c).toNat = #s

Tactic:
add_sub_cancel_left,

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ (↑(#s)).toNat = #s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
← NonemptyInterval.coe_mul_interval,

Goal state after:
case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑(a✝¹ * a✝) = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case some.some
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s

Tactic:
exact congr_arg WithBot.some (neg_add_rev _ _)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ x.coeff x.order = 0 ↔ x = 0

Tactic:
refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
  rw [order_of_ne hx]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).orderTop = x.orderTop

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).orderTop = x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).leadingCoeff = x.leadingCoeff

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x + -mk y = mk x - mk y

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x + -mk y = mk x + -mk y
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (f g),
    x_1 ∉ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g) →
      (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0

Tactic:
rintro ⟨_, _⟩ h1 h2
      contrapose! h2
      obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1
      obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2
      simp only [mem_map, mem_antidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists]
      simp only [mem_antidiagonal, embDomain_coeff, mem_support, ← hf,
        OrderEmbedding.eq_iff_eq] at h1
      exact ⟨i, j, h1, rfl⟩

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

Goal state before:
pp: 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
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - ↑y
huv' : x - ↑y - v = u
hyv : ↑y + v ∈ (↑f).domain
h✝ : f.eval x = ↑↑f y
h : True
⊢ ArchimedeanClass.mk (x - ↑y) < ArchimedeanClass.mk (x - (↑y + v))

Tactic:
← sub_sub,

Goal state after:
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
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - ↑y
huv' : x - ↑y - v = u
hyv : ↑y + v ∈ (↑f).domain
h✝ : f.eval x = ↑↑f y
h : True
⊢ ArchimedeanClass.mk (x - ↑y) < ArchimedeanClass.mk (x - ↑y - v)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ ∀ {x : Kˣ}, x ∈ {x | A.valuation (↑x - 1) < 1} → x⁻¹ ∈ {x | A.valuation (↑x - 1) < 1}

Tactic:
dsimp
    intro a ha
    conv =>
      lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]
    rwa [add_sub_cancel, ← Valuation.map_mul, sub_mul, Units.inv_mul, ← neg_sub, one_mul,
      Valuation.map_neg]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ IsUnit x ↔ mk ↑x = 0

Tactic:
by
  rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ s ⊆ a • s

Tactic:
by
  rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
obtain hx | hx := eq_or_ne (mk x) 0
  · unfold stdPart
    have hx' : 0 ≤ mk x⁻¹ := by simp_all
    rw [dif_pos hx.ge, dif_pos hx']
    · apply eq_inv_of_mul_eq_one_left
      suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
      ext
      apply inv_mul_cancel₀
      aesop
  · rw [stdPart_of_mk_ne_zero hx, stdPart_of_mk_ne_zero, inv_zero]
    rwa [mk_inv, neg_ne_zero]

Goal state after:
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) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))

Tactic:
congr 2

Goal state after:
case e_a
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
⊢ dk = P.eraseLead.degree.succ - 1 - (k - n)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: 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
y : ↥(f.extendFun hx).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) y))) ∈ (f.extendFun hx).toFun.range

Tactic:
obtain ⟨y', hy'⟩ := y
  rw [extendFun, LinearPMap.domain_supSpanSingleton] at hy'
  obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hy'
  obtain ⟨k, hk⟩ := Submodule.mem_span_singleton.mp hb
  simp_rw [extendFun, ← hab, ← hk]
  rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ ha]
  rw [ofLex_add, map_add, toLex_add, ofLex_smul, map_smul, toLex_smul]
  refine Submodule.add_mem _ ?_ (Submodule.smul_mem _ _ ?_)
  · obtain ⟨⟨a', ha'mem⟩, ha'⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range ⟨a, ha⟩ c)
    refine LinearMap.mem_range.mpr ⟨⟨a', by simpa using Submodule.mem_sup_left ha'mem⟩, ?_⟩
    rw [← ha']
    exact LinearPMap.supSpanSingleton_apply_mk_of_mem f.val _ hx ha'mem
  · apply truncLT_eval_mem_range_extendFun

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
n : ℤ
⊢ evalEval x y ↑n = ↑n

Tactic:
simp only [evalEval, eval_intCast]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = ⇑(evalEvalRingHom x x✝)

Tactic:
evalEvalRingHom_eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = ⇑(eval₂RingHom (evalRingHom x) x✝)
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.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ p.coeff m = q.coeff m

Tactic:
rw [isMonicOfDegree_iff] at hp hq

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ p.coeff m = q.coeff m
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + -q).IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
· rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]
    apply dvd_mul_right

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ p.smeval x + -q.smeval x = p.smeval x - q.smeval x

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ p.smeval x + -q.smeval x = p.smeval x + -q.smeval x
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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
⊢ (aeval r) ((⇑derivative)^[k] p) = 0

Tactic:
have h (x) : (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rw [Nat.lt_iff_add_one_le] at hk
    exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)
  rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
  simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul,
    h, ← mul_smul_comm, mul_assoc, ← mul_sum, eval_mul, pow_one, eval_sub, eval_X, eval_C, sub_self,
    zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
by_cases hpz : P = 0
  · simp_all
  · have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
    obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)
    simp [signVariations, List.destutter, leadingCoeff_eraseLead_eq_nextCoeff h₂, hl, h, h₂,
      coeffList_eraseLead hpz]

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

Goal state before:
pp: case inr.refine_2
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
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) + (aeval r) ((⇑derivative)^[q - 1] p) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

Tactic:
congr 2

Goal state after:
case inr.refine_2.e_a.e_a
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
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) = 0

case inr.refine_2.e_a.e_a
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
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ (aeval r) ((⇑derivative)^[q - 1] p) = (q - 1)! • eval r p'

case inr.refine_2.e_a
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
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: case h.of
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : α
⊢ (mk rels) (FreeMonoid.of x) ∈ closure (range (of rels))

Tactic:
exact subset_closure <| by simp [range, of]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = (algebraMap R (QuadraticAlgebra R a b)) a + (algebraMap R (QuadraticAlgebra R a b)) b * ω

Tactic:
by
  simp [omega_mul_omega_eq_add, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
z w : R
⊢ (algebraMap R (QuadraticAlgebra R a b)) z ∣ (algebraMap R (QuadraticAlgebra R a b)) w ↔ z ∣ w

Tactic:
by
  rw [algebraMap_dvd_iff]
  simp

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:
by
      have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
      simp [*, ← hs_nC_mul, nextCoeff, coeff_X_sub_C_mul]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ x = x

Tactic:
rw [← act_one x, ← Shelf.self_distrib, act_one]

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne

Tactic:
congr 2

Goal state after:
case e_2.e_2
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁.toMulZeroOneClass.toMulOneClass = inst₂.toMulZeroOneClass.toMulOneClass
Module: Mathlib.Algebra.Ring.WithZero

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

Tactic:
cases c

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

case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (0 + ↑a✝) = ↑a✝¹ * 0 + ↑a✝¹ * ↑a✝
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ n ∈ P.support ↔ ¬↑⟨P.coeff n, ⋯⟩ = 0

Tactic:
mem_support_iff

Goal state after:
K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ P.coeff n ≠ 0 ↔ ¬↑⟨P.coeff n, ⋯⟩ = 0
Module: Mathlib.Algebra.Ring.WithZero

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

Tactic:
cases c

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

case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x) P

Tactic:
aeval_eq_sum_range,

Goal state after:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c

Tactic:
cases c

Goal state after:
case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0

case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
a✝ : α
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a - b) (a - c)

Tactic:
simp only [sub_eq_add_neg, h.neg.add_right]

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
⊢ ∀ (a : RingQuot r), 0 + a = a

Tactic:
rintro ⟨⟨⟩⟩
    simp [add_quot, ← zero_quot, zero_add]

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
⊢ ∀ (a : RingQuot r), 0 • a = 0

Tactic:
rintro ⟨⟨⟩⟩
    simp [smul_quot, ← zero_quot]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
p : SkewPolynomial R
⊢ X ^ 0 * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[0] b)) * X ^ 0

Tactic:
simp only [pow_zero, one_mul, Function.iterate_zero, id_eq, sum_monomial, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a - (monomial n) b

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a + -(monomial n) b
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
congr 2

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * (unsym b + unsym c) + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)