mathlib-initiative/mathlib-tactics huggingface dataset:
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
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)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
rw [ArchimedeanClass.mk_sum hsupport' (hmono.mono (by simp))]
    rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop (by
      simpa using! (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2)]
    apply Finset.min'_lt_of_mem_erase_min' (α := FiniteArchimedeanClass M)
    apply Finset.min'_mem _ _

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
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range

Tactic:
have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
  simp_rw [seed.domain_baseEmbedding] at hmem
  obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem
  -- Truncating in the codomain is the same as truncating away some submodule
  let f' : Π₀ (i : FiniteArchimedeanClass M), seed.stratum i :=
    DFinsupp.mk f.support fun d ↦ if c.val ≤ d.val then 0 else f d.val
  refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
  · rw [seed.domain_baseEmbedding, ArchimedeanStrata.baseDomain,
      Submodule.mem_iSup_iff_exists_dfinsupp']
    use f'
  apply_fun ofLex
  rw [ofLex_toLex, LinearPMap.toFun_eq_coe]
  ext d
  rw [seed.coeff_baseEmbedding rfl]
  unfold f'
  obtain hdc | hdc := lt_or_ge d c
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc,
      seed.coeff_baseEmbedding hf.symm]
    apply congrArg
    have hcd : ¬ c.val ≤ d.val := not_le_of_gt hdc
    simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
    aesop
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]
    have hcd : c.val ≤ d.val := hdc
    simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
    convert! LinearMap.map_zero _
    simp

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
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : x - ↑y ≠ 0
⊢ f.eval x ≠ ↑↑f y

Tactic:
let xy := mk _ 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
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
⊢ f.eval x ≠ ↑↑f y
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 ∨ x⁻¹ ∉ A

Tactic:
by
  rw [← valuation_le_one_iff, ← or_congr_right' fun h ↦ (A.valuation.one_le_val_iff h).not,
    ← lt_iff_not_ge, ← mem_nonunits_iff, or_iff_right_of_imp]
  rintro rfl
  exact A.nonunits.zero_mem

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 → a • b ∈ s

Tactic:
simp_rw [← Finset.mem_inv_smul_finset_iff, Finset.subset_iff]

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
⊢ MonotoneOn stdPart {x | 0 ≤ mk x}

Tactic:
intro x (hx : 0 ≤ mk x) y (hy : 0 ≤ mk y) h

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
hy : 0 ≤ mk y
h : x ≤ y
⊢ stdPart x ≤ stdPart y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ stdPart 0 = 0

Tactic:
rw [stdPart, 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
⊢ stdPart 1 = 1

Tactic:
rw [stdPart, 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
f : ℝ →+*o K
r : ℝ
⊢ stdPart (f r) = r

Tactic:
rw [stdPart, 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: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
⊢ 0 = sInf {r | x < f r}

Tactic:
obtain h | h := le_or_gt 0 x

Goal state after:
case inr.inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : 0 ≤ x
⊢ 0 = sInf {r | x < f r}

case inr.inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : x < 0
⊢ 0 = sInf {r | x < f r}
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
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
have h₂ := withBotSucc_degree_eq_natDegree_add_one hep

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
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ R[X][Y] ≃ₐ[R] R[X][Y]

Tactic:
apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X))

Goal state after:
case h₁
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

case h₂
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
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).IsMonicOfDegree n

Tactic:
refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩

Goal state after:
case inr.refine_1
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).natDegree ≤ n

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
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:
by
  convert ha.of_dvd_add hmn hb ?_ h with q
  · rw [sub_neg_eq_add]
  · rwa [natDegree_neg]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
refine (h_irr.isUnit_or_isUnit <|
    (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_ <;>
      apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map <;>
    apply IsUnit.of_mul_eq_one

Goal state after:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ a.leadingCoeff * ?refine_1.b = 1

case refine_1.b
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ R

case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ b.leadingCoeff * ?refine_2.b = 1

case refine_2.b
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ R
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 _ _ _ ?_
  simp only [Prod.forall, mem_antidiagonal]
  rintro a b rfl
  apply MvPolynomial.isHomogeneous_monomial
  simp [Finsupp.update_eq_add_single]

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
⊢ (trinomial k m n u v w).coeff n = w

Tactic:
trinomial_def,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff n = w
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
⊢ (trinomial k m n u v w).coeff m = v

Tactic:
trinomial_def,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff m = v
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
⊢ (trinomial k m n u v w).coeff k = u

Tactic:
trinomial_def,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff k = u
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
⊢ reflect n (trinomial k m n u v w) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
trinomial_def,

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
⊢ reflect n (C u * X ^ k + C v * X ^ m + C w * X ^ n) * X ^ k = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) • 0 * eval r ((⇑derivative)^[x + 1] p') = 0

Tactic:
smul_zero,

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ 0 * eval r ((⇑derivative)^[x + 1] p') = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
⊢ p.IsUnitTrinomial

Tactic:
· have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
      Int.sq_eq_one_of_sq_le_three
        ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk)
    refine isUnitTrinomial_iff.mpr ⟨?_, fun k hk => .of_pow_eq_one (key k hk) two_ne_zero⟩
    rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_cast] at hp
    exact Nat.cast_injective hp

Goal state after:
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 * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp.coeff) }

Tactic:
rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]

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 * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp.coeff) }
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 * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp.coeff) }

Tactic:
trinomial_def,

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 * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((C ↑u * X ^ k + C ↑v * X ^ m + C ↑w * X ^ n) *
                  (C ↑w * X ^ k + C ↑v * X ^ (n - m + k) + C ↑u * X ^ n)).toFinsupp.coeff) }
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ (aeval r) ((⇑derivative)^[k] p) = q ! • 0

Tactic:
smul_zero,

Goal state after:
case right
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ (aeval r) ((⇑derivative)^[k] p) = 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right
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 : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p' + q ! • 0

Tactic:
smul_zero,

Goal state after:
case right
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 : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p' + 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_1
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
⊢ g i ^ n i ≠ 0

Tactic:
exact ((hg i hi).pow (n i)).ne_zero

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

Goal state before:
pp: 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
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]},
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) →
      ∀ i ∈ s, (∑ j, r i j * g i ^ ↑j).degree < (g i ^ n i).degree
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
obtain ⟨hq, hr⟩ := quo_mul_prod_add_sum_rem_mul_prod_unique
    (fun i hi => (hg i hi).pow (n i)) (hgg.imp fun i j hij => hij.pow) (hrd hr₁) (hrd hr₂) hf

Goal state after:
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
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]},
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) →
      ∀ i ∈ s, (∑ j, r i j * g i ^ ↑j).degree < (g i ^ n i).degree
hq : q₁ = q₂
hr : ∀ i ∈ s, ∑ j, r₁ i j * g i ^ ↑j = ∑ j, r₂ i j * g i ^ ↑j
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) + (x.imI * y.imJ) • q.k +
            (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (c₂ • q.j - q.k) + (x.imJ * y.imJ) • c₃ • 1 +
          (x.imJ * y.imK) • ((c₂ * c₃) • 1 - c₃ • q.i)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₃ • q.i +
        (x.imK * y.imK) • -((c₁ * c₃) • 1))

Tactic:
simp only [smul_smul, smul_neg, sub_eq_add_neg, ← add_assoc, neg_smul]

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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((x.imK * y.imK * (c₁ * c₃)) • 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ ↑0 = ↑0

Tactic:
inst₁.natCast_zero,

Goal state after:
case zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ 0 = ↑0
Module: Mathlib.Algebra.Ring.Semireal.Defs

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

Tactic:
rw [add_comm] at hn
      push_cast at hn
      simpa using IsSemireal.one_add_ne_zero (by simp) hn

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
rw [← neg_mul]

Goal state after:
R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -m * n ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier