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

Goal state before:
pp: case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ (↑n + 1) * (f q * |y|) ≤ (↑n + 1) * |x|

Tactic:
simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)

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

Goal state before:
pp: case inr
Γ✝ : 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 ∈ {x | 0 < (↑x - 1).orderTop}
hy : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
⊢ x * y ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
· simp_all only [Set.mem_ofPred_eq, orderTop_self_sub_one_pos_iff]
      have h1 : x.val.leadingCoeff * y.val.leadingCoeff = 1 := by rw [hx.2, hy.2, mul_one]
      constructor
      · rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
      · rw [Units.val_mul, leadingCoeff_mul_of_ne_zero (h1 ▸ one_ne_zero), h1]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
⊢ ∀ ⦃a₂ : R⦄, C r = C a₂ → r = a₂

Tactic:
s

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
⊢ C r = C s → r = 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
x y : ↥(↑f).domain
⊢ (orderHom f.toOrderAddMonoidHom) (ArchimedeanClass.mk x) = (orderHom f.toOrderAddMonoidHom) (ArchimedeanClass.mk y) ↔
    ArchimedeanClass.mk x = ArchimedeanClass.mk y

Tactic:
exact Function.Injective.eq_iff <| orderHom_injective <| toOrderAddMonoidHom_injective _

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✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∃ x_1, ¬(x * y).coeff x_1 = (x * z).coeff x_1

Tactic:
refine ⟨x.order + a, ?_⟩

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬(x * y).coeff (x.order + a) = (x * z).coeff (x.order + a)
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
c : FiniteArchimedeanClass M
x : ↥(↑f).domain
hx : ↑x ∈ ball K c
d : FiniteArchimedeanClass M
hd : ↑d ≤ ↑c
⊢ (ofLex (↑↑f x)).coeff d = 0

Tactic:
by
  obtain rfl | ne := eq_or_ne x 0
  · simp
  apply HahnSeries.coeff_eq_zero_of_lt_orderTop
  apply_fun FiniteArchimedeanClass.withTopOrderIso _
  rw [orderTop_eq_archimedeanClassMk, FiniteArchimedeanClass.withTopOrderIso_apply_coe]
  apply lt_of_le_of_lt hd
  simpa using! hx (by simpa using! ne)

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
⊢ A = B

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle <;> simp_all

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
⊢ B = ⊤

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle <;> simp_all

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
⊢ i ≤ FiniteArchimedeanClass.mk (↑y - x) hxy0

Tactic:
by_contra! hlt

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 : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hlt : FiniteArchimedeanClass.mk (↑y - x) hxy0 < i
⊢ False
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 • s = s ↔ s ⊆ a • s

Tactic:
Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le,

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a • s = s ↔ s = a • s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (if h : 0 ≤ mk 0 then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 h) else 0) = 0

Tactic:
dif_pos

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 ?hc) = 0

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (if h : 0 ≤ mk 1 then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 h) else 0) = 1

Tactic:
dif_pos

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 ?hc) = 1

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 1
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
⊢ (if h : 0 ≤ mk (x + y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

Tactic:
dif_pos

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
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
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 (x + y)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x * y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

Tactic:
dif_pos

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
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
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 (x * y)
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
r : ℝ
⊢ (if h : 0 ≤ mk (f r) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (f r) h) else 0) = r

Tactic:
dif_pos

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
r : ℝ
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (f r) ?hc) = r

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
r : ℝ
⊢ 0 ≤ mk (f r)
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
⊢ stdPart x = sSup {r | f r < x}

Tactic:
by
  rw [← neg_inj, ← stdPart_neg, stdPart_eq_sInf f, ← Real.sInf_neg]
  congr 1
  ext
  simp [neg_lt]

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) =
    (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse)[k]?

Tactic:
List.getElem?_append_right (List.length_replicate ▸ hkn),

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse[k - (List.replicate n 0).length]?
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
⊢ swap (C (C a)) * C X ^ n = C (C a) * C X ^ n

Tactic:
Bivariate.swap_C_C

Goal state after:
case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
⊢ C (C a) * C X ^ n = C (C a) * C X ^ n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

Tactic:
rw [coeff_add_eq_left_of_lt hq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a b : R
⊢ (X ^ 2 + C a * X + C b).IsMonicOfDegree 2

Tactic:
rw [add_assoc]
  exact (isMonicOfDegree_X_pow R 2).add_right <|
    calc
    _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_add_le ..
    _ = (C a * X).natDegree := by simp
    _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

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

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

Tactic:
← sub_sub_sub_cancel_right p q (X ^ n)

Goal state after:
R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
⊢ (p - X ^ n - (q - X ^ n)).natDegree < n
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ if R a b then if R b c then IsChain R (a :: b :: destutter' R c l) else IsChain R (a :: destutter' R b l)
  else if R a c then IsChain R (a :: destutter' R c l) else True

Tactic:
isChain_cons_cons,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ if R a b then if R b c then R a b ∧ IsChain R (b :: destutter' R c l) else IsChain R (a :: destutter' R b l)
  else if R a c then IsChain R (a :: destutter' R c l) else True
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ (C 1).smeval x = 1 • x ^ 0

Tactic:
smeval_C

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ 1 • x ^ 0 = 1 • x ^ 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (C u * X ^ (n - k) + C v * X ^ (revAt n) m + C w * X ^ (revAt n) n) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
revAt_le hmn.le,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (C u * X ^ (n - k) + C v * X ^ (n - m) + C w * X ^ (revAt n) n) * X ^ k = trinomial k (n - m + k) n w v u
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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - (q + k) ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) gp

Tactic:
refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) (↑((q + k).descFactorial k) * p')
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (k + k) (↑u * ↑w)).coeff +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                    (AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (k + n) (↑u * ↑u)).coeff +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (m + k) (↑v * ↑w)).coeff +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                    (AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + n) (↑v * ↑u)).coeff) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (n + k) (↑w * ↑w)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v)).coeff +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (n + n) (↑w * ↑u)).coeff)) }

Tactic:
AddMonoidAlgebra.coeff_single

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).re = (star b * star a).re

Tactic:
simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ a.re * b.re + a✝ * a.im * b.im + b✝ * (a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    (b.re + b✝ * b.im) * (a.re + b✝ * a.im) + a✝ * b.im * a.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).im = (star b * star a).im

Tactic:
simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg]

Goal state after:
case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ -(a.re * b.im + a.im * b.re + b✝ * a.im * b.im) =
    -((b.re + b✝ * b.im) * a.im) + -(b.im * (a.re + b✝ * a.im)) + b✝ * b.im * a.im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit (norm x) → IsUnit x

Tactic:
simp only [isUnit_iff_exists]

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ (∃ b_1, norm x * b_1 = 1 ∧ b_1 * norm x = 1) → ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x

Tactic:
rw [← left_cancel x]

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
by
  intro _ _ h
  -- Use above extensionality lemma to prove injectivity by showing that `h_add` and `h_mul` hold.
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Tactic:
simpa [g, r₁, r₂, add_assoc] using hf

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
⊢ ∀ (n : ℕ) (x : RingQuot r), x ^ (n + 1) = x ^ n * x

Tactic:
rintro n ⟨⟨⟩⟩
    simp only [pow_quot, mul_quot, pow_succ]

Goal state after: