mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ n * x + b * n * y = n * x + n * b * y

Tactic:
ring

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ x * (x + b * y) + -(a * y * y) = x * x + b * x * y - a * y * y

Tactic:
ring

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 0

Tactic:
ring

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.re +
      a * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) + a * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)

Tactic:
ring

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.im + (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.re +
      b * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im) + x✝².im * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) +
      b * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)

Tactic:
ring

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.re + a * x✝¹.im * x✝.im = x✝.re * x✝¹.re + a * x✝.im * x✝¹.im

Tactic:
ring

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im = x✝.re * x✝¹.im + x✝.im * x✝¹.re + b * x✝.im * x✝¹.im

Tactic:
ring

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

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

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re + x✝.re + b * (x✝¹.im + x✝.im) = x✝¹.re + b * x✝¹.im + (x✝.re + b * x✝.im)

Tactic:
ring

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
⊢ b * z.im = z.im * b

Tactic:
ring

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
⊢ z.im + z.im = z.im * (1 + 1)

Tactic:
ring

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re + a * z.im * w.im) * (z.re * w.re + a * z.im * w.im) +
        b * (z.re * w.re + a * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) -
      a * (z.re * w.im + z.im * w.re + b * z.im * w.im) * (z.re * w.im + z.im * w.re + b * z.im * w.im) =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)

Tactic:
ring

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
⊢ z.re * z.re + z.im * (b * z.re) - z.im * (a * z.im) = z.re * (z.re + b * z.im) + -(z.im * (a * z.im))

Tactic:
ring

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
⊢ 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))

Tactic:
ring

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ (x.re + b * x.im) * (x.re + b * x.im) + -(b * (x.re + b * x.im) * x.im) = x.re * x.re + b * x.re * x.im

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ z.re * (z.re + b * z.im) = z.re * z.re + b * z.re * z.im

Tactic:
ring

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)

Tactic:
ring

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.im + z.im * w.re + b * z.im * w.im = w.re * z.im + w.im * (z.re + b * z.im)

Tactic:
ring

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

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : z * (algebraMap R (QuadraticAlgebra R a b)) r = 0
⊢ z = 0

Tactic:
rw [QuadraticAlgebra.ext_iff, re_zero, im_zero] at hz

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : (z * (algebraMap R (QuadraticAlgebra R a b)) r).re = 0 ∧ (z * (algebraMap R (QuadraticAlgebra R a b)) r).im = 0
⊢ z = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
⊢ trace ω = b

Tactic:
simp [trace_def]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
⊢ trace 1 = 2

Tactic:
simp [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
⊢ z ^ 2 - (z + star z) * z + z * star z = 0

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
⊢ Multiset.countP (fun x ↦ 0 < x) P.roots ≤ P.signVariations

Tactic:
generalize h : P.roots.countP (0 < ·) = num_pos_roots

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
num_pos_roots : ℕ
h : Multiset.countP (fun x ↦ 0 < x) P.roots = num_pos_roots
⊢ num_pos_roots ≤ P.signVariations
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
i : ι
hi : i ∈ s
⊢ ∑ i_1,
      (algebraMap R[X] K) (r i (Fin.revPerm i_1) * g i ^ ↑(Fin.revPerm i_1) * ∏ k ∈ s.erase i, g k ^ n k) *
        ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
refine Fintype.sum_congr _ _ fun j => ?_

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 : ι
hi : i ∈ s
j : Fin (n i)
⊢ (algebraMap R[X] K) (r i (Fin.revPerm j) * g i ^ ↑(Fin.revPerm j) * ∏ k ∈ s.erase i, g k ^ n k) *
      ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case h.h.h
R : Type u_1
inst✝ : Rack R
X✝² X✝¹ X✝ : R
⊢ X✝² ◃⁻¹ X✝¹ ◃⁻¹ X✝ = (X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝

Tactic:
rw [self_distrib_inv]

Goal state after:
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✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
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₁ 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
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1) * (algebraMap R[X] K) (g i) ^ n i = (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
← mul_one (gi i ^ (j.rev.1 + 1)),

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
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₁ 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
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1) * 1 * (algebraMap R[X] K) (g i) ^ n i = (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ : R
⊢ (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ n : R
⊢ (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ x ∈ s, ((algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)

Tactic:
Finset.prod_inv_distrib

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * (∏ x ∈ s, (algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
⊢ F f = f.sum fun a b ↦ b • F (single a 1)

Tactic:
conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]

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✝ : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    { toQuot := Quot.mk (Rel r) ((algebraMap S R) (x * y)) } =
      { toQuot := Quot.mk (Rel r) ((algebraMap S R) x) } * { toQuot := Quot.mk (Rel r) ((algebraMap S R) y) }

Tactic:
simp [mul_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (x y : R), { toQuot := Quot.mk (Rel r) (x * y) } = { toQuot := Quot.mk (Rel r) x } * { toQuot := Quot.mk (Rel r) y }

Tactic:
simp [mul_quot]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ star Q = Q

Tactic:
simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]

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

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
p q : StarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
obtain ⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩ := p

Goal state after:
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
q : StarSubsemiring R
carrier✝ : Set R
mul_mem'✝ : ∀ {a b : R}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : R},
    a ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
star_mem'✝ :
  ∀ {a : R},
    a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝ }.carrier →
      star a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝ }.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
      star_mem' := star_mem'✝ } =
    q
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ ↑(star (f * g)) a = ↑(star g * star f) a

Tactic:
calc
      star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r).coeff (n + 1) = 0

Tactic:
simp [coeff_C]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute (1 + 1) a
⊢ ?m.16 a

Tactic:
one_add_one_eq_two

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.16 a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (single g r * x).coeff g' = 0

Tactic:
classical
  rw [coeff_mul, sum_single_index]
  · apply Finset.sum_eq_zero
    simp_rw [ite_eq_right_iff]
    rintro g'' _hg'' rfl
    exact absurd ⟨_, rfl⟩ h
  · simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = g.sum fun a b ↦ (f * single a b).coeff x

Tactic:
rw [← coeff_sum, ← mul_sum f g, g.sum_single]

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

Goal state before:
pp: R : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
n : Type u_8
inst✝⁴ : DecidableEq n
B : n → Type u_9
inst✝³ : (i : n) → AddCommMonoid (B i)
inst✝² : (i : n) → Module R (B i)
inst✝¹ : (i : n) → StarAddMonoid (B i)
inst✝ : ∀ (i : n), StarModule R (B i)
i : n
⊢ star (toConv (single R B i)) = toConv (single R B i)

Tactic:
aesop (add simp [Pi.single, Function.update])

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

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ ((star (toConv comul)).ofConv ∘ₗ single R B i) x =
    ((toConv (↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ∘ₗ comul)).ofConv ∘ₗ single R B i) x

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, intrinsicStar_apply, Pi.star_single,
    Pi.comul_single, LinearEquiv.coe_coe]

Goal state after:
R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ star ((TensorProduct.map (single R B i) (single R B i)) (comul (star x))) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))