mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Quotient (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))),
    (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x}).OrdConnected

Tactic:
refine fun x ↦ ⟨?_⟩

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 : Quotient (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))
⊢ ∀ ⦃x_1 : FiniteElement K⦄,
    x_1 ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x} →
      ∀ ⦃y : FiniteElement K⦄,
        y ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x} →
          Set.Icc x_1 y ⊆ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x}
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 : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
stdPart_of_mk_ne_zero hx,

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

Tactic:
mk_neg

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
⊢ 0 ≤ mk 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 : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ 0 ≤ mk x

Tactic:
apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _)

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r - 1 < r

K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r + 1 > r
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial.monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
a✝ : ℕ
⊢ ((PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * (monomial m) b))).coeff a✝ =
    ((monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial m) b)) +
          (monomial m) b • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))).coeff
      a✝

Tactic:
simp [Polynomial.monomial_mul_monomial, add_comm]

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

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

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:
· simpa using hp

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: 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
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) = spanCoeffs(q) ^ deg(r) * spanCoeffs(q) * spanCoeffs(p)

Tactic:
mul_assoc

Goal state after:
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
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) = spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Subsingleton R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

pp: case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

Tactic:
· simpa using hp

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n
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
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
obtain ⟨ev, bi, bu, hF⟩ :=
    denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
      (by
        rw [eq_intCast, one_div_mul_cancel]
        rw [Int.cast_ne_zero]
        exact b0.ne.symm)
  obtain Fa := congr_arg abs hF
  rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa
  rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] at Fa
  rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]
  refine Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))
  rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF
  rcases hF with hF | hF
  · exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (eq_zero_of_pow_eq_zero hF)))).elim
  · rwa [div_eq_mul_inv]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
mul_assoc

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
mul_assoc

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree))
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case empty
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
h : ∀ i ∈ ∅, (p i).natDegree ≤ n i
⊢ (∏ i ∈ ∅, p i).homogenize (∑ i ∈ ∅, n i) = ∏ i ∈ ∅, (p i).homogenize (n i)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
simp [destutter', if_pos hab, Nat.le_succ]

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

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ ∅, (g i).Monic
hgg : (↑∅).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ ∅, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r i * ∏ k ∈ ∅.erase i, g k

Tactic:
| empty =>

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ x * (X ^ n * p).smeval x = x ^ (1 + n) * p.smeval x

Tactic:
smeval_X_pow_mul n,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ x * (x ^ n * p.smeval x) = x ^ (1 + n) * p.smeval x
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 * (q.smeval y * x) = x ^ n * q.smeval y * x

Tactic:
mul_assoc

Goal state after:
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 * (q.smeval y * x) = x ^ n * (q.smeval y * x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv p = p + derivative (sumIDeriv p)

Tactic:
by
  rw [sumIDeriv_apply, derivative_sum, sum_range_succ', sum_range_succ,
    add_comm, ← add_zero (Finset.sum _ _)]
  simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one,
    Function.iterate_zero_apply, iterate_derivative_eq_zero (Nat.lt_succ_self _)]

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

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

Tactic:
| empty =>

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

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

Tactic:
| empty =>

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

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

Tactic:
simp [h₁, hc, hη.ne']

Goal state after:
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
  have hq : IsUnitTrinomial q := (isUnitTrinomial_iff'' hpq).mp hp
  obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp
  obtain ⟨k', m', n', hkm', hmn', x, y, z, hq⟩ := hq
  have hk : k = k' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
  have hn : n = n' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ←
      hp, ← natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq,
      trinomial_natDegree hkm' hmn' z.ne_zero]
  subst hk
  subst hn
  rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)
  · rw [h1] at hq
    rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
    · exact Or.inl h2
    · exact Or.inr (Or.inr (Or.inl h2))
  · rw [h1] at hq
    rw [trinomial_def] at hp
    rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp
    rw [← neg_mul_neg, ← mirror_neg] at hpq
    rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inr p.mirror_neg))

Goal state after:
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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext <;> simp [mul_add] <;> abel

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re + a * z.im * w.im) • 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • ↑u =
    (z * w).re • 1 + (z * w).im • ↑u

Tactic:
by
              simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
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 : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k + ∑ i_1, r' i i_1 * g i ^ ↑i_1 * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
mul_assoc

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
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 : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ q' i * (g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k) + ∑ i_1, r' i i_1 * g i ^ ↑i_1 * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ trace ((algebraMap R (QuadraticAlgebra R a b)) r) = 2 * r

Tactic:
grind [trace_def]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ trace (star z) = trace z

Tactic:
grind [trace_def]

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).re = (z + star z).re

Tactic:
grind [trace_def]

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).im = (z + star z).im

Tactic:
grind [trace_def]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (unit.mul a) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.mul unit) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.inv.mul a) = mapAux f unit

Tactic:
simp [toEnvelGroup.mapAux]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x y : R
⊢ mapAux f (((incl x).mul (incl y)).mul (incl x).inv) = mapAux f (incl (x ◃ y))

Tactic:
simp [toEnvelGroup.mapAux]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ ⟦x.mul y⟧.liftOn (mapAux f) ⋯ = ⟦x⟧.liftOn (mapAux f) ⋯ * ⟦y⟧.liftOn (mapAux f) ⋯

Tactic:
simp [toEnvelGroup.mapAux]

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := by
    ext : 1 <;> assumption

Goal state after:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
⊢ inst₁ = inst₂
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.i * q.j) = F q.k

Tactic:
q.i_mul_j

Goal state after:
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.k = F q.k
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
⊢ inst₁ = inst₂

Tactic:
have h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne :=
    AddCommGroupWithOne.ext h_add (congrArg (·.toOne.one) h₂)

Goal state after:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic

Tactic:
by
  rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : Relation.EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂

Tactic:
induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›

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 : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
⊢ ∀ (x y : RingQuot r), Quot.lift ⇑f ⋯ (x * y).toQuot = Quot.lift ⇑f ⋯ x.toQuot * Quot.lift ⇑f ⋯ y.toQuot

Tactic:
by
      rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩
      simp only [mul_quot, f.map_mul x y]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := ⋯
i₁ : 0 ≤ P
⊢ 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)

Tactic:
simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁

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

Goal state before:
pp: case mk.mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr ({ toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ }) =
    star' r hr { toQuot := Quot.mk (Rel r) a✝¹ } + star' r hr { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp [star'_quot, add_quot, star_add]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ f.sum single = f

Tactic:
by
  apply coeff_injective; simp only [coeff_sum', coeff_single, Finsupp.sum_single]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (g y * (f (b.coeff x) * g x)) = f (a.coeff y) * g y * (f (b.coeff x) * g x)

Tactic:
mul_assoc

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (g y * (f (b.coeff x) * g x)) = f (a.coeff y) * (g y * (f (b.coeff x) * g x))
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = (map trop 0).sum

Tactic:
| empty =>

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

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = (map untrop 0).inf

Tactic:
| empty =>

Goal state after: