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

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℕ
⊢ trace ↑n = 2 * ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℤ
⊢ trace ↑n = 2 * ↑n

Tactic:
by

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

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

Tactic:
by

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:
by

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:
by

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
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
h₁ : P.nextCoeff ≠ 0
⊢ P.signVariations = P.eraseLead.signVariations + ?succ.inr.inr.refine_1

Tactic:
by

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
⊢ (algebraMap R (QuadraticAlgebra R a b)) (trace z) = z + star z

Tactic:
by

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
⊢ star z = (algebraMap R (QuadraticAlgebra R a b)) (trace z) - z

Tactic:
by

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 - trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Tactic:
by

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 = trace z • z - (algebraMap R (QuadraticAlgebra R a b)) (norm z)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ norm z = 0 ↔ z = 0

Tactic:
by

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
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
⊢ P.nextCoeff ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z ≠ 0
⊢ z * z⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
by

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
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ (∑ j, r i j * g i ^ ↑j).degree < (g i ^ n i).degree

Tactic:
by

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
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
⊢ P.signVariations = P.eraseLead.signVariations + ?succ.inl.refine_1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

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
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
by

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
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
this✝ : P.signVariations = P.eraseLead.signVariations + 1
this : SignType.sign ((X - C η) * P).nextCoeff = -1
⊢ ((X - C η) * P).eraseLead.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
by

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✝ : 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
x : ι
hx : x ∈ s
⊢ (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1

Tactic:
by

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
P : R[X]
η : R
hη : 0 < η
hP : P ≠ 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
by

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
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
⊢ P ≠ 0

Tactic:
by

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
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
⊢ ∃ x ∈ P.roots, 0 < x

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_3
inst✝ : (i : ι) → Mul (R i)
a : (i : ι) → R i
⊢ IsRegular a ↔ ∀ (i : ι), IsRegular (a i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Prod

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : Mul R
inst✝ : Mul S
a : R
b : S
⊢ IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.ULift

Goal state before:
pp: R : Type v
inst✝ : Mul R
a : R
⊢ IsRegular { down := a } ↔ IsRegular a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y z : S
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y z : Rᵐᵒᵖ},
    op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (fun y ↦ op (unop (op x) ◃ unop y)) ((fun y ↦ op (unop (op x) ◃⁻¹ unop y)) (op y)) = op y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (fun y ↦ op (unop (op x) ◃⁻¹ unop y)) ((fun y ↦ op (unop (op x) ◃ unop y)) (op y)) = op y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x ↦ x ◃⁻¹ x) ((fun x ↦ x ◃ x) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x ↦ x ◃ x) ((fun x ↦ x ◃⁻¹ x) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
h : IsInvolutory R
x y : R
⊢ x ◃⁻¹ y = x ◃ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝³ : Shelf S₁
inst✝² : Shelf S₂
inst✝¹ : Shelf S₃
S : Type u_4
inst✝ : Shelf S
⊢ ∀ {x y : S}, x ◃ y = x ◃ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝² : Shelf S₁
inst✝¹ : Shelf S₂
inst✝ : Shelf S₃
g : S₂ →◃ S₃
f : S₁ →◃ S₂
⊢ ∀ {x y : S₁}, (g.toFun ∘ f.toFun) (x ◃ y) = (g.toFun ∘ f.toFun) x ◃ (g.toFun ∘ f.toFun) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
⊢ ∀ {x : Qᵐᵒᵖ}, x ◃ x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x y z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ (MulEquiv.symm (MulAut.conj x)) ((MulAut.conj x) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ (MulAut.conj x) ((MulEquiv.symm (MulAut.conj x)) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x : Conj G}, (MulAut.conj x) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝² : Quandle Q
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ {x y : Conj G}, f (x ◃ y) = f x ◃ f y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ Function.Involutive (dihedralAct n a)

Tactic:
by

Goal state after:
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₁ q₂ : Basis A c₁ c₂ c₃
hi : q₁.i = q₂.i
hj : q₁.j = q₂.j
⊢ q₁ = q₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x : Dihedral n}, dihedralAct n x x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : R}, act' (x ◃ y) = act' x ◃ act' y

Tactic:
by

Goal state after:
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
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ Equivalence (PreEnvelGroupRel R)

Tactic:
by

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✝ b✝ a'✝ b'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
hb : PreEnvelGroupRel' R b✝ b'✝
⊢ mapAux f (a✝.mul b✝) = mapAux f (a'✝.mul b'✝)

Tactic:
by

Goal state after:
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
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } = c₃ • 1

Tactic:
by

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✝ a'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
⊢ mapAux f a✝.inv = mapAux f a'✝.inv

Tactic:
by

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 b c : PreEnvelGroup R
⊢ mapAux f ((a.mul b).mul c) = mapAux f (a.mul (b.mul c))

Tactic:
by

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✝ : 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)
⊢ ↑j + 1 ≤ n i

Tactic:
by

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:
by

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:
by

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:
by

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:
by

Goal state after:
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
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
by

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
⊢ Quotient.liftOn 1 (mapAux f) ⋯ = 1

Tactic:
by

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
⊢ Quotient.liftOn (⟦x⟧ * ⟦y⟧) (mapAux f) ⋯ = ⟦x⟧.liftOn (mapAux f) ⋯ * ⟦y⟧.liftOn (mapAux f) ⋯

Tactic:
by

Goal state after:
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
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ r • t ↔ 0 ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
by

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✝ : 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,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      (algebraMap R[X] K) f * ∏ i ∈ s, gi i ^ n i =
        (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup G
inst✝¹ : Module R G
inst✝ : DecidableEq G
t : Finset G
a : R
⊢ -a • t = -(a • t)

Tactic:
by

Goal state after:
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₃
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k

Tactic:
by

Goal state after: