awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟧
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) = (F : (a : EnvelGroup R) → G) ⟦x.mul y⟧
have 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)
Tactic: simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
Cleared hypotheses: ih_x, ih_y, hm, this
-- 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 : 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)
have 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)
Tactic: rw [← ih_x, ← ih_y, mapAux]
-- 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 : 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)
⊢ 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)
have 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
Tactic: rw [← ih_x, ← ih_y, mapAux]
-- 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 : 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
⊢ 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)
have 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
Tactic: rw [← ih_x, ← ih_y, mapAux]
-- 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⟧
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = (F : (a : EnvelGroup R) → G) ⟦x.mul y⟧
have 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)
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]
-- 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 : 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)
⊢ 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)
have hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
Tactic: have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := 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 : 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⟧)⁻¹
⊢ 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)
have 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) sorry, map_one' := sorry, map_mul' := sorry :
              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)
Tactic: rw [hm, map_inv, map_inv, ih_x]
-- 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 : 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)
⊢ 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)
have 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) sorry, map_one' := sorry, map_mul' := sorry :
                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)
Tactic: rw [hm, map_inv, map_inv, ih_x]
-- 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 : 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)
⊢ 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)
have 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) sorry, map_one' := sorry, map_mul' := sorry :
                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)
Tactic: rw [hm, map_inv, map_inv, ih_x]
-- 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 : 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)
⊢ 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)
have inv₃ : Eq.{u_2 + 1} (α := G) (((F : (a : EnvelGroup R) → G) ⟦x⟧)⁻¹ : G) (((F : (a : EnvelGroup R) → G) ⟦x⟧)⁻¹ : G)
Tactic: rw [hm, map_inv, map_inv, ih_x]
-- 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 : PreEnvelGroup 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)
        ⟦x⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G)
have unit : 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) sorry, map_one' := sorry, map_mul' := sorry :
              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: induction x with
        | unit => exact F.map_one.symm
        | incl => rfl
        | mul x y ih_x ih_y =>
          have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
          simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
          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]
          exact F.map_mul
        | inv x ih_x =>
          have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
          rw [hm, map_inv, map_inv, ih_x]
Cleared hypotheses: x
-- 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 : PreEnvelGroup R
unit :
  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)
        ⟦PreEnvelGroup.unit⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦PreEnvelGroup.unit⟧ : 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⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G)
have incl : ∀ (x : 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) sorry, map_one' := sorry, map_mul' := sorry :
                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⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦incl x⟧ : G)
Tactic: induction x with
        | unit => exact F.map_one.symm
        | incl => rfl
        | mul x y ih_x ih_y =>
          have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
          simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
          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]
          exact F.map_mul
        | inv x ih_x =>
          have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
          rw [hm, map_inv, map_inv, ih_x]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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) =
    x
have 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, sorry⟩ =
  x (⟨HAdd.hAdd (α := ℕ) 0 3, sorry⟩ : Fin (Nat.succ 3))
Tactic: ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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))
⊢ (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
have 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, sorry⟩ =
  x (⟨HAdd.hAdd (α := ℕ) 0 2, sorry⟩ : Fin (Nat.succ 3))
Tactic: ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩