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

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∑ n ∈ range #s, (c + ↑n) ≤ ∑ x ∈ s, x

Tactic:
by
  convert! sum_Ico_le_sum hs
  refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
  · intro x mx; rw [mem_Ico]; rw [mem_range] at mx; lia
  · intro x mx y my (h : c + x = c + y); lia
  · intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
    rw [mem_coe, mem_Ico] at mx
    use (x - c).toNat; grind

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
obtain heq | hlt := h.eq_or_lt

Goal state after:
case mp.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
heq : 0 = (ofLex x).leadingCoeff
⊢ 0 ≤ x

case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
a : M
⊢ ↑u * 1 ≤ a ↔ ↑u ≤ a

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
a : M
⊢ ↑u ≤ a ↔ ↑u ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
a : M
⊢ a ≤ ↑u * 1 ↔ a ≤ ↑u

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
a : M
⊢ a ≤ ↑u ↔ a ≤ ↑u
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a : M
u : Mˣ
⊢ 1 ≤ a * ↑u⁻¹ ↔ ↑u ≤ a

Tactic:
by
  rw [u.le_mul_inv_iff, one_mul]

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : ArchimedeanClass.mk ↑a = ArchimedeanClass.mk ↑b
⊢ ArchimedeanClass.mk a = ArchimedeanClass.mk b

Tactic:
rw [ArchimedeanClass.mk_eq_mk] at this ⊢

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : (∃ m, |↑b| ≤ m • |↑a|) ∧ ∃ n, |↑a| ≤ n • |↑b|
⊢ (∃ m, |b| ≤ m • |a|) ∧ ∃ n, |a| ≤ n • |b|
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
α : Type u_2
inst✝ : Add α
f : α → R
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f (a + b) ≤ f a + f b

Tactic:
apply le_trans (hna _ _)
  rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]
  exact ⟨hf _, hf _⟩

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

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
have hhy : ((of R).symm y) ≠ 0 := hy

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop
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
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a

Tactic:
by
  induction n with
  | zero => simp
  | succ n _ =>
    rw [add_nsmul]
    apply le_trans <| hna (n • a) (1 • a)
    simpa

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
g : Multiset α → α := fun t ↦ t.prod
b : Multiset α
hb_in : powersetCard (s.card - m) s ≠ 0 → b ∈ powersetCard (s.card - m) s
hb_le : f (map g (powersetCard (s.card - m) s)).sum ≤ f (g b)
⊢ b ∈ powersetCard (s.card - m) s

Tactic:
exact hb_in (card_pos.mp
      (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := hx

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)|
⊢ ∃ n, x ≤ ↑n
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✝ : NonAssocSemiring R
x : R⟦Γ⟧
x✝ : Γ
⊢ (x * 1).coeff x✝ = x.coeff x✝

Tactic:
exact coeff_mul_single_zero.trans (mul_one _)

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
⊢ 1 * 1 = 1

Tactic:
mul_one

Goal state after:
Γ✝ : 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
⊢ 1 = 1
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
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
⊢ y⁻¹ ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
suffices 0 < (y.inv - 1).orderTop by exact this

Goal state after:
Γ✝ : 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
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
⊢ 0 < (y.inv - 1).orderTop
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ y ^ 2 * a - z ^ 2 * a ∈ P ∧ -(y ^ 2 * a) + z ^ 2 * a ∈ P

Tactic:
aesop (add simp sub_eq_add_neg)

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

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : (↑a / ↑b)⁻¹ ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rw [show (a / b : K)⁻¹ = b / a by simp] at hh

Goal state after:
case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : ↑b / ↑a ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
⊢ (max ↑a ↑b).untop₀ = max (↑a).untop₀ (↑b).untop₀

Tactic:
simp only [untop₀_coe]

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
⊢ (max ↑a ↑b).untop₀ = max a b
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G t ≤ stabilizer G s
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s
⊢ stabilizer G (s ∪ t) = stabilizer G t

Tactic:
rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]

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

Goal state before:
pp: case pos
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
hac : -0 • x < a
hc : c = 0
⊢ ↑↑f 0 < ↑↑f ⟨a, ha⟩

Tactic:
exact f.prop.strictMono (by simpa using! hac)

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
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ x < f r

Tactic:
← neg_lt_neg_iff,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ -f r < -x
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
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ x ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain

Tactic:
by simpa using Submodule.mem_sup_right (Submodule.mem_span_singleton_self x)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
⊢ ((monomial n) x).coeffList.length = (x :: List.replicate n 0).length

Tactic:
by classical simp [hx]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 1 = 1

Tactic:
by
  simp only [evalEval, eval_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
x y : R
s : S
p : R[X][Y]
⊢ evalEval x y (s • p) = s • evalEval x y p

Tactic:
simp only [evalEval, eval_smul]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m * 1)

Tactic:
mul_one

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ q.IsMonicOfDegree n

pp: case inr
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
⊢ q.IsMonicOfDegree n

Tactic:
· simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
    exact hpq.2

Goal state after:
case inr
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
⊢ q.IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ C a * 1 * X ^ n = C a * X ^ n

Tactic:
mul_one

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ C a * X ^ n = C a * X ^ n
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * 1

Tactic:
mul_one

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 *
          ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
· rw [Finset.prod_cons, Finset.sum_cons, Function.update_self, Finset.erase_cons, add_mul,
        add_add_add_comm, ← mul_assoc, ← add_mul, add_comm (_ * g i), ← mul_comm (g i),
        modByMonic_add_div, add_mul, add_assoc, add_right_inj, Finset.sum_mul,
        Finset.sum_mul, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
      refine Finset.sum_congr rfl fun j hj => ?_
      rw [Function.update_of_ne (hjs hj).symm, Finset.erase_cons_of_ne _ (hjs hj),
        Finset.prod_cons, ← Finset.mul_prod_erase s g hj]
      simp_rw [← mul_assoc, ← add_mul]
      refine congrArg (· * _) ?_
      rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ s, g i)

Tactic:
induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ ((X - C η) * (monomial d) c).nextCoeff = ((X - C η) * (monomial d) c).coeff (0 + d)

Tactic:
simp [hc, nextCoeff, natDegree_mul (X_sub_C_ne_zero η)]

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

Tactic:
add_comm (x : ℤ),

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = norm z

Tactic:
rw [← LinearMap.det_toMatrix <| basis ..]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ ((LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)).det = norm z
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃ (x ◃⁻¹ y) ◃ x ◃⁻¹ y ◃⁻¹ z = z

Tactic:
self_distrib

Goal state after:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
self_distrib

Goal state after:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
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₃
⊢ c₃ • (q.i * 1) = c₃ • q.i

Tactic:
mul_one

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₃
⊢ c₃ • q.i = c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.j * F q.i = c₂ • F q.j - F q.k

Tactic:
rw [← map_mul, q.j_mul_i, map_sub, map_smul]

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ T 1 ∈ Subsemiring.center α

Tactic:
constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
f : A →ₐ[k] B
g : G →* B
h_comm : ∀ {x : A} {y : G}, f (y • x) * g y = g y * f x
⊢ ∀ (r : k), (↑↑(liftNCRingHom (↑f) g ⋯)).toFun ((algebraMap k (SkewMonoidAlgebra A G)) r) = (algebraMap k B) r

Tactic:
simp [liftNCRingHom]

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), a * 0 = 0

Tactic:
rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, mul_zero]

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
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
toQuot✝¹ : Quot (Rel r)
x : R
toQuot✝ : Quot (Rel r)
y : R
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel r) x } * { toQuot := Quot.mk (Rel r) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) x }.toQuot * Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) y }.toQuot

Tactic:
simp only [mul_quot, f.map_mul x y]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 4 * P = 4 • P

Tactic:
simp [map_ofNat, Algebra.smul_def]

Goal state after: