mathlib-initiative/mathlib-tactics huggingface dataset:
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

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:
· by_contra! hlt
      obtain hj := sub_eq_zero_of_eq (hj (mk _ hxy0) hlt)
      contrapose! hj
      rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub, hzyclass]
      apply f.coeff_ne_zero

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
⊢ FiniteArchimedeanClass.mk (↑y - x) hxy0 ≤ i
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 y : FiniteElement K
hy : ⟦y⟧ = ⟦x⟧
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ⟦z⟧ = ⟦x⟧

Tactic:
Quotient.eq,

Goal state after:
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 y : FiniteElement K
hy : (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) y x
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) z x
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)

Tactic:
by
  rw [← smul_eq_mul, ← Set.iUnion_smul_set]
  exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
inst✝⁶ : Differential A
R : Type u_2
R₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing R₂
inst✝³ : Differential R₂
inst✝² : Algebra A R
inst✝¹ : Algebra A R₂
inst✝ : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ ((algebraMap A R) a)′ = (algebraMap A R) a′

Tactic:
by
    change (LinearMap.comp ..) _ = _
    simp [deriv_algebraMap]

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

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

Tactic:
simpa using op_smul_set_stabilizer_subset ha

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

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → b ∈ a⁻¹ • s

Tactic:
Finset.subset_iff

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

Goal state before:
pp: case pos.inl
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
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ ((truncLT c) (ofLex (↑↑f y))).coeff d = ((truncLT c) (ofLex (f.eval x))).coeff d

Tactic:
HahnSeries.coeff_truncLT_of_lt hdc

Goal state after:
case pos.inl
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
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (ofLex (↑↑f y)).coeff d = (ofLex (f.eval x)).coeff d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg.inl
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
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (ofLex (f.eval x)).coeff d = ((truncLT c) (ofLex (f.eval x))).coeff d

Tactic:
HahnSeries.coeff_truncLT_of_lt hdc

Goal state after:
case neg.inl
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
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (ofLex (f.eval x)).coeff d = (ofLex (f.eval x)).coeff d
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case ha
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
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := ⋯
⊢ (aeval (f x)) (derivative p) ≠ 0

Tactic:
Polynomial.aeval_algHom

Goal state after:
case ha
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
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (f.comp (aeval x)) (derivative p) ≠ 0
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: 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
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
| (aeval (f x)) (derivative p) * f x′

Tactic:
Polynomial.aeval_algHom

Goal state after:
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
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
| (f.comp (aeval x)) (derivative p) * f x′
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
⊢ ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b - r

Tactic:
obtain ⟨q, hq⟩ := exists_eq_mul_left_of_dvd h

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b - r
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
⊢ ?m.59 * (algebraMap ℤ K) b = 1

Tactic:
rw [eq_intCast, one_div_mul_cancel]
        rw [Int.cast_ne_zero]
        exact b0.ne.symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
⊢ ((ofFn n) v).degree < ↑n

Tactic:
by_cases h : ofFn n v = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬(ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ (MvPolynomial.aeval g) (p.homogenize n) = (aeval (g 0)) p

Tactic:
by
  apply eval₂_homogenize_of_eq_one <;> assumption

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (p.homogenize n).IsHomogeneous n

Tactic:
refine MvPolynomial.IsHomogeneous.sum _ _ _ ?_

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ ∀ i ∈ antidiagonal n, ((MvPolynomial.monomial fun₀ | 0 => i.1 | 1 => i.2) (p.coeff i.1)).IsHomogeneous 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
⊢ 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 * (g i * ∏ x ∈ s, g x) +
        (∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
      ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i * ∏ k ∈ s, g k +
        ∑ x ∈ s,
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)

Tactic:
add_add_add_comm,

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
⊢ 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 * (g i * ∏ x ∈ s, g x) +
        (q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i * ∏ k ∈ s, g k +
      ((∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) * (g i * ∏ x ∈ s, g x) +
        ∑ x ∈ s,
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)
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 ^ (revAt 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 (hkm.trans 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 ^ (revAt n) m + C w * X ^ (revAt n) n) * X ^ k = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : p = trinomial k (n - m' + k) n ↑u ↑v ↑u
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror

Tactic:
rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp

Goal state after:
case inr.inl
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : trinomial k m' n ↑u ↑v ↑u = p.mirror
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
← q.mirror_mirror,

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror.mirror.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
⊢ Irreducible p

Tactic:
refine irreducible_of_mirror hp.not_isUnit (fun q hpq => ?_) h

Goal state after:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ 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✝ : AddCommMonoid R
⊢ AddCommMonoid (QuadraticAlgebra R a b)

Tactic:
by
  refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_ <;> intros <;> rfl

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j * g i ^ ↑j).degree < (g i ^ n i).degree

Tactic:
refine (degree_mul_le _ _).trans_lt ?_

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j).degree + (g i ^ ↑j).degree < (g i ^ n i).degree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
⊢ (∑ x ∈ s, (algebraMap R[X] K) (∑ j, r x j * g x ^ ↑j * ∏ k ∈ s.erase x, g k ^ n k)) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
Finset.sum_mul

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
⊢ ∑ i ∈ s, (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
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:
by rw [← map_mul, q.j_mul_i, map_sub, map_smul]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : { f // ∀ ⦃x y : R⦄, r x y → f x = f y }
x✝ : R
⊢ ↑((fun F ↦ ⟨F.comp (mkRingHom r), ⋯⟩) ((fun f ↦ preLift ⋯) f)) x✝ = ↑f x✝

Tactic:
simp only [preLift_def, mkRingHom_def, RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk,
                 OneHom.coe_mk, Function.comp_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n m : ℕ
r s : R
⊢ (monomial n) r * (monomial m) s = (monomial (n + m)) (r * ofAdd n • s)

Tactic:
exact SkewMonoidAlgebra.single_mul_single

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r * X ^ k = (monomial (n + k)) r

Tactic:
induction k with
  | zero      => simp
  | succ n ih => simp [pow_succ, ← mul_assoc, ih, add_assoc]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
instNonempty : Nonempty G
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p 0

Tactic:
by simpa using single (Classical.choice instNonempty) 0

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
⊢ (0 + 1) • x = x

Tactic:
simp [one_nsmul]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)

Tactic:
convert! Multiset.untrop_prod (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

Goal state after: