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

Goal state before:
pp: case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk ((f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)))

Tactic:
have hferase : (f.sum fun _ x ↦ x.val) - (f (f.support.min' hsupport)).val =
      ∑ x ∈ f.support.erase (f.support.min' hsupport), (f x).val :=
    sub_eq_of_eq_add (Finset.sum_erase_add _ _ (Finset.min'_mem _ hsupport)).symm

Goal state after:
case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk ((f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)))
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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
a : HahnModule Γ' R V
⊢ ((single 0) r * x) • a = r • x • a

Tactic:
mul_smul',

Goal state after:
Γ : 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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
a : HahnModule Γ' R V
⊢ (single 0) r • x • a = r • x • a
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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : CommSemiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ (x * (single 0) r) • y = x • r • y

Tactic:
mul_smul',

Goal state after:
Γ : 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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : CommSemiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ x • (single 0) r • y = x • r • y
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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
⊢ ↑↑f x = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))

Tactic:
have heq : (⟨x.val, hx'⟩ : seed.baseEmbedding.domain).val = x.val := rfl

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
⊢ ↑↑f x = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C r).order = 0

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ (C r).order = 0

Tactic:
· rw [h, C_zero, order_zero]

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ (C r).order = 0
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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ (ofLex (↑↑f y)).coeff (seq n) = f.evalCoeff x (seq n)

Tactic:
refine (f.evalCoeff_eq ((ball_strictAnti K).antitone ?_ hy)).symm

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ seq n ≤ seq 0
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f < 0 ↔ f < 0

Tactic:
by
  simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P

Tactic:
by
  refine Ideal.ext (fun x => ?_)
  apply IsLocalization.AtPrime.to_map_mem_maximal_iff
  exact isLocalRing (ofPrime A P)

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔ x = 0 ∨ A.valuation x < 1

Tactic:
← mem_nonunits_iff,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔ x = 0 ∨ x ∈ A.nonunits
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : UpperSet α
⊢ s * 1 = s

Tactic:
by
      rw [mul_comm]
      exact one_mul _

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : LowerSet α
⊢ s * 1 = s

Tactic:
by
      rw [mul_comm]
      exact one_mul _

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
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
r : ℝ
hr : r ∈ {r | x < f r}
⊢ ↑a ≤ r

Tactic:
by_contra! hra

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
r : ℝ
hr : r ∈ {r | x < f r}
hra : r < ↑a
⊢ False
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (C p) = eval x p

Tactic:
by
  rw [evalEval, eval_C]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case convert_7
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A), (Algebra.linearMap A R) a′ = ((algebraMap A R) a)′

Tactic:
· simp [deriv_algebraMap]

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 :
  ↑0 =
    (algebraMap ℤ K) b ^ f.natDegree *
      eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
Int.cast_zero,

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 :
  0 =
    (algebraMap ℤ K) b ^ f.natDegree *
      eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) p.natTrailingDegree) = p.coeff p.natDegree

Tactic:
revAt_le (Nat.le_add_left _ _),

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.coeff (p.natDegree + p.natTrailingDegree - p.natTrailingDegree) = p.coeff p.natDegree
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:
by
    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.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
⊢ (X ^ 0 * p).smeval x = x ^ 0 * p.smeval x

Tactic:
simp [npow_zero, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.natDegree ≤ 1

Tactic:
rwa [not_le, Nat.lt_succ_iff] at hdeg2

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

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : ∑ x ∈ p.support, 1 = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Tactic:
sum_const,

Goal state after:
case refine_2
p : ℤ[X]
hp : #p.support • 1 = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right.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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = (q - 1)! • eval r 0

Tactic:
eval_zero,

Goal state after:
case right.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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = (q - 1)! • 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
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
this✝ : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
this : 0 < ((X - C η) * P.eraseLead).natDegree
⊢ List.map (⇑SignType.sign) ((X - C η) * P).eraseLead.coeffList =
    List.map (⇑SignType.sign) ((X - C η) * P.eraseLead).coeffList

Tactic:
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]

Goal state after:
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
⊢ 2 * k = 2 * k'

Tactic:
←
      trinomial_natTrailingDegree hkm hmn u.ne_zero,

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
⊢ 2 * (trinomial k m n ↑u ?m.168 ?m.169).natTrailingDegree = 2 * k'

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
⊢ ℤ

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
⊢ ℤ
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
r : R
⊢ ((algebraMap R (QuadraticAlgebra R a b)) r).re • 1 + ((algebraMap R (QuadraticAlgebra R a b)) r).im • ↑u =
    (algebraMap R A) r

Tactic:
simp [← Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ star z = (algebraMap R (QuadraticAlgebra R a b)) (trace z) - z

Tactic:
by
  rw [algebraMap_trace_eq_add_star, add_sub_cancel_left]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by ext <;> simp [sq]; field_simp; simp [NNRat.cast_def]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case unit
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x : EnvelGroup R
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦unit⟧ =
    F ⟦unit⟧

Tactic:
exact F.map_one.symm

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
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Tactic:
obtain ⟨q, r, hr, hf⟩ := div_prod_eq_quo_add_sum_rem_div K f hg hcoprime

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q : R[X]
r : Bool → R[X]
hr : ∀ i ∈ Finset.univ, (r i).degree < (g i).degree
hf : ↑f / ∏ i, ↑(g i) = ↑q + ∑ i, ↑(r i) / ↑(g i)
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : A → A → Prop
k : S
a b : A
h : Rel r a b
⊢ Rel r (k • a) (k • b)

Tactic:
by
  simp only [Algebra.smul_def, Rel.mul_right h]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, f.coeff x • (of k G) x • v ∈ ↑W

Tactic:
exact Submodule.sum_smul_mem W _ fun g _ ↦ h g v hv

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
⊢ p.support = ∅ ↔ p = 0

Tactic:
simp [support]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ (star (f * g)) a = (star (g * f)) a

Tactic:
CommMonoid.mul_comm f g

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ (star (g * f)) a = (star (g * f)) a
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
simp only [update_def, support_eq_skewMonoidAlgebra_support, SkewMonoidAlgebra.support_update]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
⊢ Finset.map toAdd.toEmbedding
      (if a = 0 then (SkewMonoidAlgebra.support p).erase (ofAdd n)
      else insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    if a = 0 then (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n
    else insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))
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
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
⊢ b₁ = b₂

Tactic:
rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj

Goal state after:
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
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj✝ : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
inj : a • single ?m.62 b₁ = a • single ?m.62 b₂
⊢ b₁ = b₂

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
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
⊢ Type ?u.36
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ (f.sum single).coeff = f.coeff

Tactic:
simp only [coeff_sum', coeff_single, Finsupp.sum_single]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
R : Type u_5
inst✝¹ : Monoid R
inst✝ : DistribMulAction R k
b : R
⊢ (mapDomain f) (b • v) = b • (mapDomain f) v

Tactic:
← coeff_inj,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
R : Type u_5
inst✝¹ : Monoid R
inst✝ : DistribMulAction R k
b : R
⊢ ((mapDomain f) (b • v)).coeff = (b • (mapDomain f) v).coeff
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = ∑ᶠ (p : G × G) (_ : p ∈ {p | p.1 * p.2 = x}), f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
have : ({p : G × G | p.1 * p.2 = x}
      ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite := by
    apply Set.Finite.inter_of_right
    apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))
    aesop
  rw [← finsum_mem_inter_support, finsum_mem_eq_finite_toFinset_sum _ this]
  classical
  let s := Set.Finite.toFinset (s := ({p : G × G | p.1 * p.2 = x}
    ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2)) this
  let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
  calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

Goal state after:
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 → WithTop R
⊢ trop (⨅ i, f i) = ∑ i, trop (f i)

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]

Goal state after: