mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
k : Γ'
hki : k < f i
hkmem : k ∉ Set.range ⇑f
⊢ (embDomain f (ofLex a)).coeff k = (embDomain f (ofLex b)).coeff k

Tactic:
embDomain_of_notMem_range hkmem

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal (b +ᵥ a) ⋯, ((single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    r • ((of R).symm x).coeff a

Tactic:
simp only [hx, smul_zero]
    rw [sum_congr _ fun _ _ => rfl, sum_empty]
    ext ⟨a1, a2⟩
    simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_vaddAntidiagonal, iff_false]
    rintro rfl h2 h1
    rw [IsCancelVAdd.left_cancel a1 a2 a h1] at h2
    exact h2 hx

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons a s h =>
    obtain ⟨b, hb1, hb2⟩ := multiset_image_add_of_nonempty (s := a ::ₘ s)
      hna g Multiset.cons_ne_zero
    exact ⟨b, fun _ ↦ hb1, hb2⟩

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x✝ : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ x✝, x.coeff ij.1 * y.coeff ij.2 = ∑ x_1 ∈ antidiagonal ⋯ ⋯ x✝, x.coeff x_1.2 * y.coeff x_1.1

Tactic:
exact Finset.sum_equiv (Equiv.prodComm _ _) (fun _ ↦ swap_mem_antidiagonal.symm) <| by simp

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

Goal state before:
pp: case mp.left
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).orderTop = orderTop 1

Tactic:
exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

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

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
⊢ (↑x).leadingCoeff * (↑y).leadingCoeff = 1

Tactic:
rw [hx.2, hy.2, mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ closure (Set.range fun s ↦ star s * s) = closure ((Set.range fun s ↦ star s * s) ×ˢ Set.range fun s ↦ star s * s)

Tactic:
Set.prod_range_range_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ closure (Set.range fun s ↦ star s * s) = closure (Set.range fun p ↦ (star p.1 * p.1, star p.2 * p.2))
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
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : K
h : 0 ≤ mk x
⊢ 0 ≤ mk (-x)

Tactic:
rwa [mk_neg]

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

Goal state before:
pp: case a
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
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
⊢ FiniteArchimedeanClass.mk (↑y - x) hxy0 ≤ i

Tactic:
contrapose! hi

Goal state after:
case a
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
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : i < FiniteArchimedeanClass.mk (↑y - x) hxy0
⊢ (ofLex (↑↑f y)).coeff i ≤ (ofLex (↑↑f z)).coeff i
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
hz : 0 ≤ mk z
⊢ mk (z * x) ≤ mk (z * y)

Tactic:
← map_zero mk

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
hz : mk 0 ≤ mk z
⊢ mk (z * x) ≤ mk (z * y)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b • a ∈ s

Tactic:
mem_stabilizer_set.1 hb

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ a ∈ s
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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this✝ : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
this : f.eval (-c • x) < ↑↑f ⟨a, ha⟩
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval x

Tactic:
eval_smul,

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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this✝ : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
this : -c • f.eval x < ↑↑f ⟨a, ha⟩
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval x
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
⊢ 0 ≤ mk (-y)

Tactic:
rwa [mk_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 y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x * y⁻¹) = stdPart x * (stdPart y)⁻¹

Tactic:
stdPart_mul hx,

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 * stdPart y⁻¹ = stdPart x * (stdPart y)⁻¹

K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ 0 ≤ mk y⁻¹
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i (Df + Dg) = i b ^ N * eval (i a * bf) (Polynomial.map i (f + g))

Tactic:
rw [map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
    congr
    refine @inv_unique K _ (i b) bg bf ?_ ?_ <;> rwa [mul_comm]

Goal state after:
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 ((algebraMap ℤ K) a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
eq_intCast

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

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

Tactic:
| monomial k c =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize n) = p

Tactic:
rw [aeval_homogenize_of_eq_one] <;> simp [*]

Goal state after:
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:
by
  induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons_cons a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

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

Goal state before:
pp: case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (p i).homogenize (n i) * (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) =
    (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

pp: case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (∏ i ∈ s, p i).natDegree ≤ ∑ i ∈ s, n i

Tactic:
ihs h.2

Goal state after:
case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i) = (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (∏ i ∈ s, p i).natDegree ≤ ∑ i ∈ s, n i
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
b : α
l₁ l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: b :: l₁)
⊢ (a :: b :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
simpa [destutter_cons_cons, rel_of_isChain_cons_cons hl₁]
      using! hl₁.tail.length_le_length_destutter (hl.cons_cons _)

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

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ p ≠ 0

Tactic:
by
  rintro rfl
  simpa using hp.card_support_eq_three

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

Goal state before:
pp: case e'_2.e'_5
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'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ eval r ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • ((X - C r) * (X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0

Tactic:
eval_smul,

Goal state after:
case e'_2.e'_5
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'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) • eval r ((X - C r) * (X - C r) ^ (q - (q - (x + 1)) - 1)) *
      eval r ((⇑derivative)^[x + 1] p') =
    0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ ((monomial d) c).signVariations = 0

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0

Tactic:
· simp [hcz]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0
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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
obtain ⟨d, hd⟩ := Nat.exists_eq_add_one.mpr (natDegree_pos_of_nextCoeff_ne_zero hc.ne)
  have hndxP : natDegree ((X - C η) * P) = P.natDegree + 1 := by
    have hPn0 : P ≠ 0 :=
      leadingCoeff_ne_zero.mp hP₀.ne'
    rw [natDegree_mul (X_sub_C_ne_zero η) hPn0, natDegree_X_sub_C, add_comm]
  have hndxeP : natDegree ((X - C η) * P.eraseLead) = P.natDegree := by
    have hePn0 : P.eraseLead ≠ 0 :=
      mt nextCoeff_eq_zero_of_eraseLead_eq_zero hc.ne
    rw [natDegree_mul (X_sub_C_ne_zero η) hePn0, natDegree_X_sub_C, add_comm]
    exact natDegree_eraseLead_add_one hc.ne
  have hQ : ((X - C η) * P).nextCoeff = coeff P d - η * coeff P (d + 1) := by
    grind [nextCoeff_of_natDegree_pos, coeff_X_sub_C_mul]
  have hQ₁ : ((X - C η) * P).nextCoeff < 0 := by
    rw [hQ, sub_neg]
    trans 0
    · grind [nextCoeff_of_natDegree_pos]
    · exact hd ▸ mul_pos hη hP₀
  have hndexP0 : natDegree (eraseLead ((X - C η) * P)) = P.natDegree := by
    apply Nat.add_right_cancel (m := 1)
    rw [← hndxP, natDegree_eraseLead_add_one hQ₁.ne]
  --the theorem is true mainly because all the signs are the same;
  --in fact, the coefficients are all the same except the first.
  suffices eraseLead (eraseLead ((X - C η) * P)) = eraseLead ((X - C η) * P.eraseLead) by
    suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
    have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
    grind [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, leadingCoeff_eraseLead_eq_nextCoeff,
      LT.lt.ne, sign_neg, coeffList_eraseLead, ne_zero_of_natDegree_gt,
      nextCoeff_eq_zero_of_eraseLead_eq_zero]
  rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_eraseLead_eq_nextCoeff hQ₁.ne]
  rw [hndexP0, ← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
  rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
  rw [hndxeP, hndxP]
  rw [leadingCoeff_eraseLead_eq_nextCoeff hc.ne, ← self_sub_monomial_natDegree_leadingCoeff]
  rw [hQ, mul_sub, sub_mul, sub_mul, X_mul_monomial, C_mul_monomial, monomial_sub]
  rw [leadingCoeff, nextCoeff_of_natDegree_pos (hd ▸ d.succ_pos), hd, Nat.add_sub_cancel]
  abel

Goal state after:
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 : (↑u + ↑v + ↑w) ^ 2 = (↑x + ↑v + ↑z) ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
rw [add_assoc, add_assoc, add_comm (u : ℤ), add_comm (x : ℤ), add_assoc, add_assoc] at hadd

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 : (↑v + (↑w + ↑u)) ^ 2 = (↑v + (↑z + ↑x)) ^ 2
⊢ q = p ∨ q = p.mirror
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✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ (r + s) • x = r • x + s • x

Tactic:
by ext <;> simp [add_smul]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2

Tactic:
simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℕ
⊢ norm ↑n = ↑n ^ 2

Tactic:
simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℤ
⊢ norm ↑n = ↑n ^ 2

Tactic:
simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
let g : Bool → R[X] := Bool.rec g₂ g₁
  let r₁ : Bool → R[X] := Bool.rec r₂₁ r₁₁
  let r₂ : Bool → R[X] := Bool.rec r₂₂ r₁₂
  have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
  have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
  have hr₁ (i : Bool) (_ : i ∈ Finset.univ) : (r₁ i).degree < (g i).degree := Bool.rec hr₂₁ hr₁₁ i
  have hr₂ (i : Bool) (_ : i ∈ Finset.univ) : (r₂ i).degree < (g i).degree := Bool.rec hr₂₂ hr₁₂ i
  refine (quo_add_sum_rem_div_unique K hg hcoprime hr₁ hr₂ ?_).imp_right fun h =>
    ⟨h true (Finset.mem_univ true), h false (Finset.mem_univ false)⟩
  simpa [g, r₁, r₂, add_assoc] using hf

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑(n + 1) = 0
⊢ n + 1 = 0

Tactic:
rw [add_comm] at hn

Goal state after:
case succ
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑(1 + n) = 0
⊢ n + 1 = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.of
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : r x✝ y✝
⊢ Relation.EqvGen (Rel r) x✝ y✝

Tactic:
exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)

Goal state after:
Module: Mathlib.Algebra.RingQuot

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

Tactic:
simp only [mul_quot, add_quot, left_distrib]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑(mkAlgHom S s) = mkRingHom s

Tactic:
mkAlgHom_def,

Goal state after:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑{ toRingHom := mkRingHom s, commutes' := ⋯ } = mkRingHom s
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Tactic:
liftAlgHom_def,

Goal state after:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ({ toFun := fun f' ↦ preLiftAlgHom S ⋯, invFun := fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ((mkAlgHom S s) x) =
    f x