awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
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
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
have rw₁ : -b / (2 * a) = -b / (2 * a)
Tactic: rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
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
⊢ False
have this₁ : 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))]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
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
⊢ False
have linarith : HMul.hMul (α := K) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
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
⊢ False
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
have rw : (x ◃ y) ◃ x = (x ◃ y) ◃ x
Tactic: rw [act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = x ◃ y
have h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
Tactic: have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ (x ◃ y) ◃ x = x ◃ y
have rw : (x ◃ y) ◃ x ◃ 1 = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ y) ◃ x = x ◃ y
have rw₁ : x ◃ y ◃ 1 = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ y) ◃ x = x ◃ y
have rw₂ : x ◃ y = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x : S
⊢ x ◃ x = x
have rw : (x ◃ 1) ◃ x ◃ 1 = x ◃ 1
Tactic: rw [← act_one x, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x : S
rw : (x ◃ 1) ◃ x ◃ 1 = x ◃ 1
⊢ x ◃ x = x
have rw₁ : x ◃ 1 ◃ 1 = x ◃ 1
Tactic: rw [← act_one x, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x : S
rw : (x ◃ 1) ◃ x ◃ 1 = x ◃ 1
rw₁ : x ◃ 1 ◃ 1 = x ◃ 1
⊢ x ◃ x = x
have rw₂ : x ◃ 1 = x ◃ 1
Tactic: rw [← act_one x, ← Shelf.self_distrib, act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
have rw : x ◃ x ◃ y = x ◃ x ◃ y
Tactic: rw [act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ y
have h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
Tactic: have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
⊢ x ◃ x ◃ y = x ◃ y
have rw : (x ◃ 1) ◃ x ◃ y = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, one_act]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ x ◃ x ◃ y = x ◃ y
have rw₁ : x ◃ 1 ◃ y = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, one_act]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ x ◃ x ◃ y = x ◃ y
have rw₂ : x ◃ y = x ◃ y
Tactic: rw [h, ← Shelf.self_distrib, one_act]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y z : S
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z
have rw : (x ◃ y) ◃ z = (x ◃ y) ◃ x ◃ z
Tactic: rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
S : Type u_1
inst : UnitalShelf S
x y z : S
rw : (x ◃ y) ◃ z = (x ◃ y) ◃ x ◃ z
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z
have rw₁ : (x ◃ y) ◃ z = ((x ◃ y) ◃ x) ◃ (x ◃ y) ◃ z
Tactic: rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z
have rw₂ : (x ◃ y) ◃ z = (x ◃ y) ◃ (x ◃ y) ◃ z
Tactic: rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z
have rw₃ : (x ◃ y) ◃ z = (x ◃ y) ◃ z
Tactic: rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' ↔ y = y'
have mp : x ◃ y = x ◃ y' → y = y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y y' : R
mp : x ◃ y = x ◃ y' → y = y'
⊢ x ◃ y = x ◃ y' ↔ y = y'
have mpr : y = y' → x ◃ y = x ◃ y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
have mp : x ◃⁻¹ y = x ◃⁻¹ y' → y = y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y y' : R
mp : x ◃⁻¹ y = x ◃⁻¹ y' → y = y'
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
have mpr : y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
have rw : (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
Tactic: rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
have rw : y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
Tactic: rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
⊢ y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
have rw : y ◃ y ◃⁻¹ z = z
Tactic: rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
⊢ y ◃ y ◃⁻¹ z = z
have rw : z = z
Tactic: rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
have repeat' : y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
Tactic: repeat' rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y z : R
repeat' repeat'₁ repeat'₂ : y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
have repeat'₃ : y ◃ y ◃⁻¹ z = z
Tactic: repeat' rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
x y : R
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹
have rw : act' (x ◃ y) * act' x = act' x * act' y
Tactic: rw [eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
x y : R
⊢ act' (x ◃ y) * act' x = act' x * act' y
have H : ∀ (z : R), Eq (α := R) ((act' (x ◃ y) * act' x : (a : R) → R) z : R) ((act' x * act' y : (a : R) → R) z : R)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
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)))
have 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)))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
y z : Rᵐᵒᵖ
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)))
have 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)))
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
z : Rᵐᵒᵖ
X 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)))
have 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))))
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
X X_1 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))))
have h : X ◃⁻¹ X_1 ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2
Tactic: simp only [op_inj, unop_op]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
X X_1 X_2 : R
⊢ X ◃⁻¹ X_1 ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2
have h : (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2 = (X ◃⁻¹ X_1) ◃⁻¹ X ◃⁻¹ X_2
Tactic: rw [self_distrib_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (x ◃ x) ◃ y = x ◃ y
have rw : (x ◃ x) ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y
Tactic: rw [← right_inv x y, ← self_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
have rw₁ : x ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y
Tactic: rw [← right_inv x y, ← self_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
have h : (op x ◃ op x) ◃ op y = op x ◃ op y
Tactic: have h := @self_act_act_eq _ _ (op x) (op y)
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
have rw : (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y
Tactic: rw [← left_cancel (x ◃ x)]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y
have rw : y = (x ◃ x) ◃ x ◃⁻¹ y
Tactic: rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y
have rw : y = x ◃ x ◃⁻¹ y
Tactic: rw [self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ y = x ◃ x ◃⁻¹ y
have rw : y = y
Tactic: rw [right_inv]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y
have h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
Tactic: have h := @self_act_invAct_eq _ _ (op x) (op y)
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y
have mp : x ◃ x = y ◃ y → x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
mp : x ◃ x = y ◃ y → x = y
⊢ x ◃ x = y ◃ y ↔ x = y
have mpr : x = y → x ◃ x = y ◃ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
have trans : x = (x ◃ x) ◃⁻¹ x ◃ x
Tactic: trans (x ◃ x) ◃⁻¹ x ◃ x
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
trans : x = (x ◃ x) ◃⁻¹ x ◃ x
⊢ x = y
have trans₁ : (x ◃ x) ◃⁻¹ x ◃ x = y
Tactic: trans (x ◃ x) ◃⁻¹ x ◃ x
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x
have rw : (x ◃ x) ◃ x = (x ◃ x) ◃ (x ◃ x) ◃⁻¹ x ◃ x
Tactic: rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x
have rw₁ : (x ◃ x) ◃ x = x ◃ x
Tactic: rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x
have rw₂ : x ◃ x = x ◃ x
Tactic: rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
have rw : (y ◃ y) ◃⁻¹ y ◃ y = y
Tactic: rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
x y : R
h : x ◃ x = y ◃ y
rw : (y ◃ y) ◃⁻¹ y ◃ y = y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
have rw₁ : (y ◃ y) ◃ (y ◃ y) ◃⁻¹ y ◃ y = (y ◃ y) ◃ y
Tactic: rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
have rw₂ : y ◃ y = (y ◃ y) ◃ y
Tactic: rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
have rw₃ : y ◃ y = y ◃ y
Tactic: rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
have h : op x ◃ op x = op y ◃ op y ↔ op x = op y
Tactic: have h := @self_act_eq_iff_eq _ _ (op x) (op y)
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
h : IsInvolutory R
x y : R
⊢ x ◃⁻¹ y = x ◃ y
have rw : x ◃ x ◃⁻¹ y = x ◃ x ◃ y
Tactic: rw [← left_cancel x, right_inv, h x]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
h : IsInvolutory R
x y : R
rw : x ◃ x ◃⁻¹ y = x ◃ x ◃ y
⊢ x ◃⁻¹ y = x ◃ y
have rw₁ : y = x ◃ x ◃ y
Tactic: rw [← left_cancel x, right_inv, h x]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
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
⊢ x ◃⁻¹ y = x ◃ y
have rw₂ : y = y
Tactic: rw [← left_cancel x, right_inv, h x]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
have rw : (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
Tactic: rw [self_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_2
inst : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
have rw : x ◃ z = z ↔ x ◃ z = z
Tactic: rw [left_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
Q : Type u_1
inst : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x
have rw : x ◃ x ◃⁻¹ x = x ◃ x
Tactic: rw [← left_cancel x]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
Q : Type u_1
inst : Quandle Q
x : Qᵐᵒᵖ
⊢ x ◃ x = x
have h : ∀ (X : Q), op X ◃ op X = op X
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
Q : Type u_1
inst : Quandle Q
G : Type u_2
inst_1 : Group G
x y z : Conj G
⊢ 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)
have dsimp : x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹
Tactic: dsimp only [MulAut.conj_apply]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b
have dsimp : 2 * a - (2 * a - b) = b
Tactic: dsimp only [dihedralAct]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
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)
have simp : 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)
Tactic: simp only [dihedralAct]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
Q : Type u_1
inst : Quandle Q
n : ℕ
x : Dihedral n
⊢ dihedralAct n x x = x
have simp : 2 * x - x = x
Tactic: simp only [dihedralAct]
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
⊢ Equivalence (PreEnvelGroupRel R)
have refl : ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
refl : ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x
⊢ Equivalence (PreEnvelGroupRel R)
have symm : ∀ {x y : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
refl : ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x
symm : ∀ {x y : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y x
⊢ Equivalence (PreEnvelGroupRel R)
have trans : ∀ {x y z : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y z → PreEnvelGroupRel R x z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
G : Type u_2
inst_1 : Group G
f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)
⊢ Quotient.liftOn (s := setoid R) 1 (mapAux f) ⋯ = 1
have change : ⟦unit⟧.liftOn (mapAux f) sorry = 1
Tactic: change Quotient.liftOn ⟦Rack.PreEnvelGroup.unit⟧ (toEnvelGroup.mapAux f) _ = 1
-- Lean 4 proof step from Mathlib.Algebra.Quandle (hypothesis)
Goal:
R : Type u_1
inst : Rack R
G : Type u_2
inst_1 : Group G
F : MonoidHom.{u_1, u_2} (EnvelGroup R) G
x_1 : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦x⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G)
ih_y :
  Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦y⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦y⟧ : G)
⊢ Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦x.mul y⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x.mul y⟧ : G)
have hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
Tactic: have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
-- Lean 4 proof step from Mathlib.Algebra.Quandle (goal)
Goal:
R : Type u_1
inst : Rack R
G : Type u_2
inst_1 : Group G
F : MonoidHom.{u_1, u_2} (EnvelGroup R) G
x_1 : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦x⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G)
ih_y :
  Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦y⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦y⟧ : G)
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
⊢ Eq.{u_2 + 1} (α := G)
    (((fun (f : ShelfHom.{u_1, u_2} R (Quandle.Conj G)) ↦
              { toFun := fun (x : EnvelGroup R) ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_1, u_2} (EnvelGroup R) G })
            ((fun (F : MonoidHom.{u_1, u_2} (EnvelGroup R) G) ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F) :
          (a : EnvelGroup R) → G)
        ⟦x.mul y⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x.mul y⟧ : G)
have mul : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = (F : (a : EnvelGroup R) → G) ⟦x.mul y⟧
Tactic: simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]