-- 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)
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) ⋯, 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.incl x⟧ :
        G)
      ((F : (a : EnvelGroup R) → G) ⟦PreEnvelGroup.incl 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⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x⟧ : G)
have mul : ∀ (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) 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))
  (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) 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)
          ⟦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) 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.mul y⟧ :
      G)
    ((F : (a : EnvelGroup R) → G) ⟦x.mul y⟧ : 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