awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quandle
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
trans : ∀ {x y z : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y z → PreEnvelGroupRel R x z
⊢ Equivalence (PreEnvelGroupRel R)

Tactic:
constructor
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
⊢ ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x

Tactic:
apply PreEnvelGroupRel.refl

Premises used: Rack.PreEnvelGroupRel.refl
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
⊢ ∀ {x y : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y x

Tactic:
apply PreEnvelGroupRel.symm

Premises used: Rack.PreEnvelGroupRel.symm
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
⊢ ∀ {x y z : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y z → PreEnvelGroupRel R x z

Tactic:
apply PreEnvelGroupRel.trans

Premises used: Rack.PreEnvelGroupRel.trans
-- Module: Mathlib.Algebra.Quandle
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)
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:
simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
a a' : PreEnvelGroup R
ha : PreEnvelGroupRel' R a a'
⊢ mapAux f a.inv = mapAux f a'.inv

Tactic:
simp [toEnvelGroup.mapAux, well_def f ha]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
a b c : PreEnvelGroup R
⊢ mapAux f ((a.mul b).mul c) = mapAux f (a.mul (b.mul c))

Tactic:
apply mul_assoc

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Quandle
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)
a : PreEnvelGroup R
⊢ mapAux f (mul unit a) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
a : PreEnvelGroup R
⊢ mapAux f (a.mul unit) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
a : PreEnvelGroup R
⊢ mapAux f (a.inv.mul a) = mapAux f unit

Tactic:
simp [toEnvelGroup.mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
x y : R
⊢ mapAux f (((incl x).mul (incl y)).mul (incl x).inv) = mapAux f (incl (x ◃ y))

Tactic:
simp [toEnvelGroup.mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
change : ⟦unit⟧.liftOn (mapAux f) ⋯ = 1
⊢ Quotient.liftOn (s := setoid R) 1 (mapAux f) ⋯ = 1

Tactic:
change Quotient.liftOn ⟦Rack.PreEnvelGroup.unit⟧ (toEnvelGroup.mapAux f) _ = 1

Premises used: Rack.PreEnvelGroup.unit, Quotient.mk, Rack.toEnvelGroup.mapAux, Quotient.liftOn
-- Module: Mathlib.Algebra.Quandle
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)
⊢ ⟦unit⟧.liftOn (mapAux f) ⋯ = 1

Tactic:
simp only [Quotient.lift_mk, mapAux]

Premises used: Quotient.lift_mk, Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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)
x_1 y_1 : EnvelGroup R
x y : PreEnvelGroup R
⊢ ⟦x.mul y⟧.liftOn (mapAux f) ⋯ = ⟦x⟧.liftOn (mapAux f) ⋯ * ⟦y⟧.liftOn (mapAux f) ⋯

Tactic:
simp [toEnvelGroup.mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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 : EnvelGroup R
⊢ 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)
        ⟦unit⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦unit⟧ : G)

Tactic:
F.map_one.symm

Premises used: Rack.toEnvelGroup.mapAux, MonoidHom.map_one, Eq.symm
-- Module: Mathlib.Algebra.Quandle
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 : EnvelGroup R
⊢ 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)
        ⟦unit⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦unit⟧ : G)

Tactic:
exact F.map_one.symm

Premises used: MonoidHom.map_one, Eq.symm
-- Module: Mathlib.Algebra.Quandle
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 : EnvelGroup R
x_1 : R
⊢ 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)
        ⟦incl x_1⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦incl x_1⟧ : G)

Tactic:
rfl
-- Module: Mathlib.Algebra.Quandle
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)
⊢ ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧

Tactic:
have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
-- Module: Mathlib.Algebra.Quandle
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⟧
mul : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = (F : (a : EnvelGroup R) → G) ⟦x.mul 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)

Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]

Premises used: Quotient.lift_mk, OneHom.coe_mk, MonoidHom.coe_mk
-- Module: Mathlib.Algebra.Quandle
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⟧
this :
  ∀ (x y : EnvelGroup R),
    (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)
simp_all :
  ∀ (ih_x : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x = (F : (a : EnvelGroup R) → G) ⟦x⟧)
    (ih_y : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y = (F : (a : EnvelGroup R) → G) ⟦y⟧)
    (hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧)
    (this :
      ∀ (x y : EnvelGroup R),
        (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
          HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)),
    mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G) ((F : (a : EnvelGroup R) → G) ⟦y⟧ : G)
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = (F : (a : EnvelGroup R) → G) ⟦x.mul y⟧

Tactic:
simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]

Premises used: Quotient.lift_mk, OneHom.coe_mk, MonoidHom.coe_mk
-- Module: Mathlib.Algebra.Quandle
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 : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x = (F : (a : EnvelGroup R) → G) ⟦x⟧
ih_y : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y = (F : (a : EnvelGroup R) → G) ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this :
  ∀ (x y : EnvelGroup R),
    (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)
rw :
  mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
    HMul.hMul (β := G) (mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x) ((F : (a : EnvelGroup R) → G) ⟦y⟧ : G)
rw₁ :
  mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
    mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x * mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y
rw₂ rw₃ :
  mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x * mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y =
    mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x * mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
    HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G) ((F : (a : EnvelGroup R) → G) ⟦y⟧ : G)

Tactic:
rw [← ih_x, ← ih_y, mapAux]

Premises used: Rack.toEnvelGroup.mapAux
-- Module: Mathlib.Algebra.Quandle
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⟧
mul :
  ∀ (x y : EnvelGroup R),
    (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = (F : (a : EnvelGroup R) → G) ⟦x.mul y⟧

Tactic:
suffices ∀ x y, F (Mul.mul x y) = F (x) * F (y) by
            simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
            rw [← ih_x, ← ih_y, mapAux]
-- Module: Mathlib.Algebra.Quandle
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⟧
⊢ ∀ (x y : EnvelGroup R),
    (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)

Tactic:
F.map_mul

Premises used: MonoidHom.map_mul
-- Module: Mathlib.Algebra.Quandle
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⟧
⊢ ∀ (x y : EnvelGroup R),
    (F : (a : EnvelGroup R) → G) (Mul.mul x y) =
      HMul.hMul (α := G) (β := G) ((F : (a : EnvelGroup R) → G) x : G) ((F : (a : EnvelGroup R) → G) y : G)

Tactic:
exact F.map_mul

Premises used: MonoidHom.map_mul
-- Module: Mathlib.Algebra.Quandle
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 : 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)
⊢ ⟦x.inv⟧ = (⟦x⟧)⁻¹

Tactic:
have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
-- Module: Mathlib.Algebra.Quandle
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 : 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)
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
inv :
  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)
inv₁ :
  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)
inv₂ :
  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)
inv₃ inv₄ : Eq.{u_2 + 1} (α := G) (((F : (a : EnvelGroup R) → G) ⟦x⟧)⁻¹ : G) (((F : (a : EnvelGroup R) → G) ⟦x⟧)⁻¹ : 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.inv⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x.inv⟧ : G)

Tactic:
rw [hm, map_inv, map_inv, ih_x]

Premises used: map_inv
-- Module: Mathlib.Algebra.Quandle
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)
⊢ ShelfHom.comp (Quandle.Conj.map ((map : (a : R →◃ Quandle.Conj G) → EnvelGroup R →* G) f)) (toEnvelGroup R) = f

Tactic:
toEnvelGroup.map.symm_apply_apply f

Premises used: Equiv.symm_apply_apply, Rack.toEnvelGroup.map, ShelfHom.comp
-- Module: Mathlib.Algebra.Quandle
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)
g : MonoidHom.{u_1, u_2} (EnvelGroup R) G
h : f = (Quandle.Conj.map g).comp (toEnvelGroup R)
⊢ g = (map : (a : R →◃ Quandle.Conj G) → EnvelGroup R →* G) f

Tactic:
h.symm ▸ (toEnvelGroup.map.apply_symm_apply g).symm

Premises used: Equiv.apply_symm_apply, Rack.toEnvelGroup.map, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Quandle
Goal:
R : Type u_1
inst : Rack R
x y : R
⊢ (((envelAction : (a : EnvelGroup R) → R ≃ R)
            ((toEnvelGroup R : (a : R) → Quandle.Conj (EnvelGroup R)) x : Quandle.Conj (EnvelGroup R)) :
          R ≃ R) :
        (a : R) → R)
      y =
    x ◃ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
h :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ : Fin (Nat.succ 3))
h₁ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (Nat.succ 3))
h₂ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (Nat.succ 3))
h₃ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) ⟨0, ⋯⟩ =
    x (⟨0, ⋯⟩ : Fin (Nat.succ 3))
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) =
    x

Tactic:
ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ : Fin (Nat.succ 3))

Tactic:
rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (Nat.succ 3))

Tactic:
rfl