awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ -(4 * a * (a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c)) ≤ 0

Tactic:
neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a))))

Premises used: Iff.mpr, mul_nonneg, HMul.hMul, neg_nonpos, HDiv.hDiv, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
h₁ : b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c))
⊢ b * b - 4 * a * c ≤ 0

Tactic:
convert! neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1

Premises used: Iff.mpr, mul_nonneg, HMul.hMul, neg_nonpos, HDiv.hDiv, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c))

Tactic:
field
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), a * (x * x) + b * x + c ≤ 0
⊢ ∀ (x : K), 0 ≤ -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_nonneg]

Premises used: neg_add, neg_nonneg, neg_mul
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
⊢ ∀ (x : K), 0 ≤ a * (x * x) + b * x + c

Tactic:
have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c < 0

Tactic:
lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_

Premises used: discrim_le_zero, lt_of_le_of_ne
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
refine : ∀ (h' : discrim a b c = 0), False
⊢ discrim a b c < 0

Tactic:
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_

Premises used: discrim_le_zero, lt_of_le_of_ne
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
⊢ 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c

Tactic:
have := h (-b / (2 * a))
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this_1 : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
rw : a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c = 0
rw₁ rw₂ : -b / (2 * a) = -b / (2 * a)
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0

Tactic:
rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]

Premises used: HMul.hMul, mul_assoc, HDiv.hDiv, quadratic_eq_zero_iff_of_discrim_eq_zero, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this_1 : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0

Tactic:
have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
    rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this_1 : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this_2 : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
linarith linarith₁ linarith₂ linarith₃ linarith₄ linarith₅ : HMul.hMul (α := K) 1 1 = 1
linarith₆ :
  HMul.hMul (α := K) 1 0 -
        (1 * a * (1 * (-b / (2 * a)) * (1 * (-b / (2 * a)))) + 1 * b * (1 * (-b / (2 * a))) + 1 * c) +
      (1 * a * (1 * (-b / (2 * a))) * (1 * (-b / (2 * a))) + 1 * b * (1 * (-b / (2 * a))) + 1 * c -
        HMul.hMul (α := K) 1 0) =
    0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), a * (x * x) + b * x + c < 0
⊢ ∀ (x : K), 0 < -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_pos]

Premises used: neg_pos, neg_add, neg_mul
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
rw rw₁ : (x ◃ y) ◃ x = (x ◃ y) ◃ x
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1

Tactic:
rw [act_one]

Premises used: UnitalShelf.act_one
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1

Tactic:
have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
rw : (x ◃ y) ◃ x ◃ 1 = x ◃ y
rw₁ : x ◃ y ◃ 1 = x ◃ y
rw₂ rw₃ : x ◃ y = x ◃ y
⊢ (x ◃ y) ◃ x = x ◃ y

Tactic:
rw [h, ← Shelf.self_distrib, act_one]

Premises used: Shelf.self_distrib, UnitalShelf.act_one
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x : S
rw : (x ◃ 1) ◃ x ◃ 1 = x ◃ 1
rw₁ : x ◃ 1 ◃ 1 = x ◃ 1
rw₂ rw₃ : x ◃ 1 = x ◃ 1
⊢ x ◃ x = x

Tactic:
rw [← act_one x, ← Shelf.self_distrib, act_one]

Premises used: Shelf.self_distrib, UnitalShelf.act_one
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
rw rw₁ : x ◃ x ◃ y = x ◃ x ◃ y
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y

Tactic:
rw [act_one]

Premises used: UnitalShelf.act_one
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y

Tactic:
have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
rw : (x ◃ 1) ◃ x ◃ y = x ◃ y
rw₁ : x ◃ 1 ◃ y = x ◃ y
rw₂ rw₃ : x ◃ y = x ◃ y
⊢ x ◃ x ◃ y = x ◃ y

Tactic:
rw [h, ← Shelf.self_distrib, one_act]

Premises used: Shelf.self_distrib, UnitalShelf.one_act
-- Module: Mathlib.Algebra.Quandle
Goal:
S : Type u_1
inst : UnitalShelf S
x y z : S
rw : (x ◃ y) ◃ z = (x ◃ y) ◃ x ◃ z
rw₁ : (x ◃ y) ◃ z = ((x ◃ y) ◃ x) ◃ (x ◃ y) ◃ z
rw₂ : (x ◃ y) ◃ z = (x ◃ y) ◃ (x ◃ y) ◃ z
rw₃ rw₄ : (x ◃ y) ◃ z = (x ◃ y) ◃ z
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z

Tactic:
rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]

Premises used: Shelf.self_distrib, UnitalShelf.act_self_act_eq, UnitalShelf.act_act_self_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (act' x : (a : R) → R) y = x ◃ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ ((act' x).symm : (a : R) → R) y = x ◃⁻¹ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ ((act' x)⁻¹ : (a : R) → R) y = x ◃⁻¹ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃⁻¹ x ◃ y = y

Tactic:
left_inv x y

Premises used: Rack.left_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃ x ◃⁻¹ y = y

Tactic:
right_inv x y

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y y' : R
mp : x ◃ y = x ◃ y' → y = y'
mpr : y = y' → x ◃ y = x ◃ y'
⊢ x ◃ y = x ◃ y' ↔ y = y'

Tactic:
constructor
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' → y = y'

Tactic:
apply (act' x).injective

Premises used: Rack.act', Equiv.injective
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃ y = x ◃ y

Tactic:
rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y y' : R
mp : x ◃⁻¹ y = x ◃⁻¹ y' → y = y'
mpr : y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

Tactic:
constructor
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'

Tactic:
apply (act' x).symm.injective

Premises used: Rack.act', Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : R
rw : (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

Tactic:
rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]

Premises used: Shelf.self_distrib, Rack.right_inv, Rack.left_cancel, Rack.invAct
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : R
rw : y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z

Tactic:
rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : R
rw : y ◃ y ◃⁻¹ z = z
⊢ y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z

Tactic:
rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : R
rw rw₁ : z = z
⊢ y ◃ y ◃⁻¹ z = z

Tactic:
rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : R
repeat' repeat'₁ repeat'₂ : y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
repeat'₃ : y ◃ y ◃⁻¹ z = z
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z

Tactic:
repeat' rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
x y : R
rw : act' (x ◃ y) * act' x = act' x * act' y
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹

Tactic:
rw [eq_mul_inv_iff_mul_eq]

Premises used: eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
x y : R
H : ∀ (z : R), Eq (α := R) ((act' (x ◃ y) * act' x : (a : R) → R) z : R) ((act' x * act' y : (a : R) → R) z : R)
⊢ act' (x ◃ y) * act' x = act' x * act' y

Tactic:
ext z
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
x y z : R
⊢ Eq (α := R) ((act' (x ◃ y) * act' x : (a : R) → R) z : R) ((act' x * act' y : (a : R) → R) z : R)

Tactic:
apply self_distrib.symm

Premises used: Shelf.self_distrib, Eq.symm
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y z : Rᵐᵒᵖ
h :
  ∀ (X : R),
    op (unop (op X) ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) =
      op (unop (op (unop (op X) ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop z)))
⊢ op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
induction x
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
y z : Rᵐᵒᵖ
X : R
h :
  ∀ (X_1 : R),
    op (unop (op X) ◃⁻¹ unop (op (unop (op X_1) ◃⁻¹ unop z))) =
      op (unop (op (unop (op X) ◃⁻¹ unop (op X_1))) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop z)))
⊢ op (unop (op X) ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) =
    op (unop (op (unop (op X) ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop z)))

Tactic:
induction y
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
z : Rᵐᵒᵖ
X X_1 : R
h :
  ∀ (X_2 : R),
    op (unop (op X) ◃⁻¹ unop (op (unop (op X_1) ◃⁻¹ unop (op X_2)))) =
      op (unop (op (unop (op X) ◃⁻¹ unop (op X_1))) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop (op X_2))))
⊢ op (unop (op X) ◃⁻¹ unop (op (unop (op X_1) ◃⁻¹ unop z))) =
    op (unop (op (unop (op X) ◃⁻¹ unop (op X_1))) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop z)))

Tactic:
induction z
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
X X_1 X_2 : R
h : X ◃⁻¹ X_1 ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2
⊢ op (unop (op X) ◃⁻¹ unop (op (unop (op X_1) ◃⁻¹ unop (op X_2)))) =
    op (unop (op (unop (op X) ◃⁻¹ unop (op X_1))) ◃⁻¹ unop (op (unop (op X) ◃⁻¹ unop (op X_2))))

Tactic:
simp only [op_inj, unop_op]

Premises used: MulOpposite.op_inj, MulOpposite.unop_op
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
X X_1 X_2 : R
h h₁ : (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2
⊢ X ◃⁻¹ X_1 ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2

Tactic:
rw [self_distrib_inv]

Premises used: Rack.self_distrib_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (fun (y : Rᵐᵒᵖ) ↦ op (unop (op x) ◃ unop y)) ((fun (y : Rᵐᵒᵖ) ↦ op (unop (op x) ◃⁻¹ unop y)) (op y)) = op y

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (fun (y : Rᵐᵒᵖ) ↦ op (unop (op x) ◃⁻¹ unop y)) ((fun (y : Rᵐᵒᵖ) ↦ op (unop (op x) ◃ unop y)) (op y)) = op y

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ op x ◃ op y = op (x ◃⁻¹ y)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ op x ◃⁻¹ op y = op (x ◃ y)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
rw : (x ◃ x) ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y
rw₁ rw₂ : x ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y
⊢ (x ◃ x) ◃ y = x ◃ y

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

Premises used: Shelf.self_distrib, Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (op x ◃ op x) ◃ op y = op x ◃ op y

Tactic:
have h := @self_act_act_eq _ _ (op x) (op y)
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : (op x ◃ op x) ◃ op y = op x ◃ op y
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
rw : (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y
⊢ (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rw [← left_cancel (x ◃ x)]

Premises used: Rack.left_cancel, Shelf.act
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
rw : y = (x ◃ x) ◃ x ◃⁻¹ y
⊢ (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y

Tactic:
rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
rw : y = x ◃ x ◃⁻¹ y
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y

Tactic:
rw [self_act_act_eq]

Premises used: Rack.self_act_act_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
rw rw₁ : y = y
⊢ y = x ◃ x ◃⁻¹ y

Tactic:
rw [right_inv]

Premises used: Rack.right_inv
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y

Tactic:
have h := @self_act_invAct_eq _ _ (op x) (op y)
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
mp : x ◃ x = y ◃ y → x = y
mpr : x = y → x ◃ x = y ◃ y
⊢ x ◃ x = y ◃ y ↔ x = y

Tactic:
constructor
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x : R
⊢ x ◃ x = x ◃ x

Tactic:
rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
trans : x = (x ◃ x) ◃⁻¹ x ◃ x
trans₁ : (x ◃ x) ◃⁻¹ x ◃ x = y
⊢ x = y

Tactic:
trans (x ◃ x) ◃⁻¹ x ◃ x

Premises used: Shelf.act
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
rw : (x ◃ x) ◃ x = (x ◃ x) ◃ (x ◃ x) ◃⁻¹ x ◃ x
rw₁ : (x ◃ x) ◃ x = x ◃ x
rw₂ rw₃ : x ◃ x = x ◃ x
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

Tactic:
rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]

Premises used: Rack.right_inv, Rack.left_cancel, Shelf.act, Rack.self_act_act_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
rw : (y ◃ y) ◃⁻¹ y ◃ y = y
rw₁ : (y ◃ y) ◃ (y ◃ y) ◃⁻¹ y ◃ y = (y ◃ y) ◃ y
rw₂ : y ◃ y = (y ◃ y) ◃ y
rw₃ rw₄ : y ◃ y = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y

Tactic:
rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]

Premises used: Rack.right_inv, Rack.left_cancel, Shelf.act, Rack.self_act_act_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ op x ◃ op x = op y ◃ op y ↔ op x = op y

Tactic:
have h := @self_act_eq_iff_eq _ _ (op x) (op y)
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
h : op x ◃ op x = op y ◃ op y ↔ op x = op y
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Quandle
Goal:
R_1 : Type u_1
inst : Rack R_1
R : Type u_2
inst_1 : Rack R
x : R
⊢ (fun (x : R) ↦ x ◃⁻¹ x) ((fun (x : R) ↦ x ◃ x) x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
R_1 : Type u_1
inst : Rack R_1
R : Type u_2
inst_1 : Rack R
x : R
⊢ (fun (x : R) ↦ x ◃ x) ((fun (x : R) ↦ x ◃⁻¹ x) x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
h : IsInvolutory R
x y : R
rw : x ◃ x ◃⁻¹ y = x ◃ x ◃ y
rw₁ : y = x ◃ x ◃ y
rw₂ rw₃ : y = y
⊢ x ◃⁻¹ y = x ◃ y

Tactic:
rw [← left_cancel x, right_inv, h x]

Premises used: Rack.right_inv, Rack.left_cancel
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
x y z : R
rw : (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [self_distrib]

Premises used: Shelf.self_distrib
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_2
inst : Rack R
x y z : R
rw rw₁ : x ◃ z = z ↔ x ◃ z = z
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [left_cancel]

Premises used: Rack.left_cancel
-- Module: Mathlib.Algebra.Quandle
Goal:
S₁ : Type u_1
S₂ : Type u_2
inst : Shelf S₁
inst_1 : Shelf S₂
f : S₁ →◃ S₂
⊢ f.toFun = (⇑f : (a : S₁) → S₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
S₁ : Type u_1
S₂ : Type u_2
inst : Shelf S₁
inst_1 : Shelf S₂
f : S₁ →◃ S₂
x y : S₁
⊢ Eq.{u_2 + 1} (α := S₂) ((f : (a : S₁) → S₂) (x ◃ y) : S₂) ((f : (a : S₁) → S₂) x ◃ (f : (a : S₁) → S₂) y : S₂)

Tactic:
map_act' f

Premises used: ShelfHom.map_act'
-- Module: Mathlib.Algebra.Quandle
Goal:
S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst : Shelf S₁
inst_1 : Shelf S₂
inst_2 : Shelf S₃
S : Type u_4
inst_3 : Shelf S
⊢ ∀ {x y : S}, x ◃ y = x ◃ y

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst : Shelf S₁
inst_1 : Shelf S₂
inst_2 : 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:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst : Shelf S₁
inst_1 : Shelf S₂
inst_2 : Shelf S₃
g : S₂ →◃ S₃
f : S₁ →◃ S₂
x : S₁
⊢ Eq.{u_3 + 1} (α := S₃) ((g.comp f : (a : S₁) → S₃) x : S₃) ((g : (a : S₂) → S₃) ((f : (a : S₁) → S₂) x : S₂) : S₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
x : Q
rw : x ◃ x ◃⁻¹ x = x ◃ x
⊢ x ◃⁻¹ x = x

Tactic:
rw [← left_cancel x]

Premises used: Rack.left_cancel
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
x : Qᵐᵒᵖ
h : ∀ (X : Q), op X ◃ op X = op X
⊢ x ◃ x = x

Tactic:
induction x
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
X : Q
⊢ op X ◃ op X = op X

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
x y z : Conj G
dsimp : x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹
⊢ Eq (α := Conj G)
    ((((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G)
        ((((MulAut.conj : (a : G) → MulAut G) y : MulAut G) : (a : G) → G) z : G) :
      G)
    ((((MulAut.conj : (a : G) → MulAut G) ((((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G) y) :
            MulAut G) :
          (a : G) → G)
        ((((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G) z : G) :
      G)

Tactic:
dsimp only [MulAut.conj_apply]

Premises used: MulAut.conj_apply
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
x y z : Conj G
⊢ x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
x y : Conj G
⊢ (MulEquiv.symm ((MulAut.conj : (a : G) → MulAut G) x) : (a : G) → G)
      ((((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G) y : G) =
    y

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
x y : Conj G
⊢ (((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G)
      ((MulEquiv.symm ((MulAut.conj : (a : G) → MulAut G) x) : (a : G) → G) y : G) =
    y

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
⊢ ∀ {x : Conj G}, (((MulAut.conj : (a : G) → MulAut G) x : MulAut G) : (a : G) → G) x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
G : Type u_2
inst : Group G
x y : Conj G
⊢ x ◃ y = x * y * x⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quandle
Goal:
G : Type u_2
inst : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x

Tactic:
grind [eq_mul_inv_iff_mul_eq]

Premises used: eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
H : Type u_3
inst_1 : Group G
inst_2 : Group H
f : G →* H
⊢ ∀ {x y : Conj G},
    Eq.{u_3 + 1} (α := Conj H) ((f : (a : G) → H) (x ◃ y) : H) ((f : (a : G) → H) x ◃ (f : (a : G) → H) y : Conj H)

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
n : ℕ
a b : ZMod n
dsimp : 2 * a - (2 * a - b) = b
⊢ dihedralAct n a (dihedralAct n a b) = b

Tactic:
dsimp only [dihedralAct]

Premises used: Quandle.dihedralAct
-- Module: Mathlib.Algebra.Quandle
Goal:
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b

Tactic:
simp
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
n : ℕ
x y z : Dihedral n
simp : 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)
⊢ dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
simp only [dihedralAct]

Premises used: Quandle.dihedralAct
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)

Tactic:
ring_nf
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
n : ℕ
x : Dihedral n
simp : 2 * x - x = x
⊢ dihedralAct n x x = x

Tactic:
simp only [dihedralAct]

Premises used: Quandle.dihedralAct
-- Module: Mathlib.Algebra.Quandle
Goal:
Q : Type u_1
inst : Quandle Q
n : ℕ
x : Dihedral n
⊢ 2 * x - x = x

Tactic:
ring_nf
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y

Tactic:
ad_conj x y

Premises used: Equiv.trans, Rack.ad_conj
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y

Tactic:
exact ad_conj x y

Premises used: Rack.ad_conj
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u
inst : Rack R
a b : PreEnvelGroup R
⊢ ∀ (a_1 : PreEnvelGroupRel' R a b), PreEnvelGroupRel R a b

Tactic:
PreEnvelGroupRel.rel

Premises used: Rack.PreEnvelGroupRel.rel
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u
inst : Rack R
a : PreEnvelGroup R
⊢ PreEnvelGroupRel R a a

Tactic:
PreEnvelGroupRel.rel PreEnvelGroupRel'.refl

Premises used: Rack.PreEnvelGroupRel'.refl, Rack.PreEnvelGroupRel.rel