mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : NoZeroDivisors R
x✝ y✝ x y : R⟦Γ⟧
hxy : x * y = 0
⊢ x = 0 ∨ y = 0

Tactic:
by
    contrapose! hxy
    simp only [ne_eq, HahnSeries.ext_iff, funext_iff, not_forall]
    exact ⟨x.order + y.order, by simpa [coeff_mul_order_add_order]⟩

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

Goal state before:
pp: case a
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
← Set.IsWF.min_add

Goal state after:
case a
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M),
    ↑c < ArchimedeanClass.mk (x - ↑z) → (ofLex (f.eval x)).coeff c = (ofLex (↑↑f z)).coeff c
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (x - ↑z)
⊢ (ofLex (↑↑f z)).coeff c = (ofLex (f.eval x)).coeff c

Tactic:
exact (h1 c hc).symm

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
h : R ≤ S
⊢ ∀ (x y : R.ValueGroup), Quotient.map' id ⋯ (x * y) = Quotient.map' id ⋯ x * Quotient.map' id ⋯ y

Tactic:
rintro ⟨⟩ ⟨⟩; rfl

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

Goal state before:
pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (S.valuation ((algebraMap (↥R) K) r))⁻¹ ≤ 1

Tactic:
← inv_one,

Goal state after:
case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (S.valuation ((algebraMap (↥R) K) r))⁻¹ ≤ 1⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup

Tactic:
· rintro h x (hx : A.valuation x = 1)
    apply_fun A.mapOfLE B h at hx
    simpa using hx

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B

Tactic:
by
  constructor
  · intro h x hx
    rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    by_cases h_2 : 1 + x = 0
    · simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]
    rcases hx with hx | hx
    · have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
      simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)
    · have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
      exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)
  · rintro h x (hx : A.valuation x = 1)
    apply_fun A.mapOfLE B h at hx
    simpa using hx

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : H
⊢ ∀ (x : G), x • s = s → f x = a → a • ⇑f '' s = ⇑f '' s

Tactic:
rintro a ha rfl

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
⊢ f a • ⇑f '' s = ⇑f '' s
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 s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G (s ∪ t) = stabilizer G s

Tactic:
by
  refine le_antisymm ?_ ?_
  · calc
      stabilizer G (s ∪ t)
        ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
      _ = stabilizer G s := by rw [union_sdiff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]
  · calc
      stabilizer G s
        ≤ stabilizer G s ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union

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

Goal state before:
pp: case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk ↑(↑n / ↑d) ⋯) * ↑d = ↑(↑n / ↑d) * ↑d

Tactic:
← map_natCast mk d,

Goal state after:
case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk ↑(↑n / ↑d) ⋯) * mk ↑d = ↑(↑n / ↑d) * mk ↑d
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
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 + stdPart y = stdPart y

Tactic:
zero_add

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : 0 ≤ mk y
⊢ stdPart y = stdPart y
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
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ stdPart (x + y) = 0

Tactic:
stdPart_of_mk_ne_zero

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ 0 = 0

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk (x + y) ≠ 0
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
⊢ stdPart x = sInf {r | x < f r}

Tactic:
stdPart_of_mk_ne_zero hx.ne

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
⊢ 0 = sInf {r | x < f r}
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: 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
⊢ ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧ d = P.natDegree - P.eraseLead.degree.succ

Tactic:
use P.natDegree - P.eraseLead.natDegree - 1
    have := eraseLead_natDegree_le P
    lia

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p : R[X][Y]
⊢ evalEval x y (-p) = -evalEval x y p

Tactic:
simp only [evalEval, eval_neg]

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

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
simp only [mul_ite, mul_one, mul_zero, hr', divModByMonicAux, degree_zero, le_bot_iff,
        degree_eq_bot, ne_eq, not_true_eq_false, and_false, ↓reduceDIte, coeff_zero, add_zero,
        Submodule.zero_mem, and_true]
      split_ifs
      exacts [H₀ _, zero_mem _]

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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by_cases hpq : p + q = 0

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ 0 + p.natTrailingDegree = p.natTrailingDegree

Tactic:
zero_add

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree = p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
← mirror_natTrailingDegree

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
hq₂ : (r₂ + g * q₂) /ₘ g = q₂
hrr₂ : (r₂ + g * q₂) %ₘ g = r₂
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
exact ⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩

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

Goal state before:
pp: case add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x

Tactic:
ph,

Goal state after:
case add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ r • p.smeval x + (r • q).smeval x = r • (p + q).smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝ : Semiring R
r : R
⊢ ⇑(leval r) = fun p ↦ p.smeval r

Tactic:
ext
  simpa using eval_eq_smeval _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ sumIDeriv (map f p) = map f (sumIDeriv p)

Tactic:
let n := max (p.map f).natDegree p.natDegree

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ sumIDeriv (map f p) = map f (sumIDeriv p)
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
⊢ 0 + w = w

Tactic:
zero_add

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ w = w
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
have cop : IsCoprime (g i) (∏ i ∈ s, g i) := by
      clear *-hgg
      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:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
hf :
  q₁ * ∏ i ∈ Finset.cons i s hi, g i + ∑ i_1 ∈ Finset.cons i s hi, r₁ i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k =
    q₂ * ∏ i ∈ Finset.cons i s hi, g i + ∑ i_1 ∈ Finset.cons i s hi, r₂ i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
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 : (trinomial k m' n ↑u ↑v ↑u).mirror = p
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror

Tactic:
mirror_eq_iff

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

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

Tactic:
rw [← right_inv x y, ← self_distrib]

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y

Tactic:
· exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
by
  rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]
  aesop

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✝ : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ (↑(-↑f)).toFun (a * b) = a * (↑(-↑f)).toFun b

Tactic:
simp [map_mul_left]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
⊢ ∀ (c : k) (x : SkewMonoidAlgebra A G), (domCongr e) (c • x) = c • (domCongr e) x

Tactic:
by
    simp only [domCongr_apply]
    intro c x
    simp_rw [equivMapDomain_eq_mapDomain, mapDomain_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
x✝ : RingQuot r
n : ℕ
a✝ : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)

Tactic:
induction n with
      | zero => rw [pow_zero, pow_zero]
      | succ n ih =>
        simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)

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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
x y : A
h_rel : rel x y
⊢ ((mkAlgHom S (rel on ⇑f.symm)).comp ↑f) x = ((mkAlgHom S (rel on ⇑f.symm)).comp ↑f) y

Tactic:
apply RingQuot.mkAlgHom_rel
        simpa [Function.onFun]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝

Tactic:
simp [Function.update_apply]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : SMulCommClass S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ { coeff := x✝² • x✝¹ • coeff✝ } = { coeff := x✝¹ • x✝² • coeff✝ }

Tactic:
smul_comm

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
⊢ ∃ inv,
    Hom.stalkMap α x ≫ inv = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
let β : Y ⟶ X := CategoryTheory.inv α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ ∃ inv,
    Hom.stalkMap α x ≫ inv = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c = 𝟙 Y.presheaf

Tactic:
by
    ext U
    rw [NatTrans.comp_app]
    simpa using! congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom g.base) ⁻¹' ⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base) '' ↑U =
    ⇑(ConcreteCategory.hom f.base) '' ↑U

Tactic:
Set.image_comp,

Goal state after:
case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom g.base) ⁻¹' ⇑(ConcreteCategory.hom g.base) '' ⇑(ConcreteCategory.hom f.base) '' ↑U =
    ⇑(ConcreteCategory.hom f.base) '' ↑U