-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
j : Discrete (Fin ((Opposite.unop Y).len + 1))
⊢ Eq (α :=
    Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
      (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
          Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
          (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G)))
        (CategoryStruct.comp (Y := ∏ᶜ fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
            (limit.lift (Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
                (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                  fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
                  Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                    ((SimplexCategory.Hom.toOrderHom f.unop :
                        (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                      i)) :
              Quiver.Hom (V := Action (Type u) G)
                (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
                  Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
                  (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                    fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
                    Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                      ((SimplexCategory.Hom.toOrderHom f.unop :
                          (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                        i)))
                (limit (J := Discrete (Fin ((Opposite.unop Y).len + 1)))
                  (Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)))
            (Iso.hom
                (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G)) :
              Quiver.Hom (V := Action (Type u) G)
                (∏ᶜ fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
                (Functor.obj (classifyingSpaceUniversalCover G) Y)) :
          Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            (Functor.obj (classifyingSpaceUniversalCover G) Y))
        (NatTrans.app
            (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))) j :
          Quiver.Hom (V := Action (Type u) G)
            (Functor.obj
              (Functor.obj (Functor.const (Discrete (Fin ((Opposite.unop Y).len + 1))))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))))
              j)
            (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j)) :
      Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
        (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
          Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
          (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G)))
        (CategoryStruct.comp (Y := Functor.obj (classifyingSpaceUniversalCover G) X)
            (Iso.hom
                (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop X).len + 1)) ↦ G)) :
              Quiver.Hom (V := Action (Type u) G)
                (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                (Functor.obj (classifyingSpaceUniversalCover G) X))
            (CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f :
              Quiver.Hom (V := Action (Type u) G) (Functor.obj (classifyingSpaceUniversalCover G) X)
                (Functor.obj (classifyingSpaceUniversalCover G) Y)) :
          Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            (Functor.obj (classifyingSpaceUniversalCover G) Y))
        (NatTrans.app
            (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))) j :
          Quiver.Hom (V := Action (Type u) G)
            (Functor.obj
              (Functor.obj (Functor.const (Discrete (Fin ((Opposite.unop Y).len + 1))))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))))
              j)
            (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j)) :
      Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
        (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
have rw : Eq (α :=
  Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
    (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
  (NatTrans.app
      (Cone.π
        (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
          fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
          Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            ((SimplexCategory.Hom.toOrderHom f.unop :
                (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
              i)))
      j :
    Quiver.Hom (V := Action (Type u) G)
      (Functor.obj
        (Functor.obj (Functor.const (Discrete (Fin ((Opposite.unop Y).len + 1))))
          (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
            Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
            (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
              fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
              Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                ((SimplexCategory.Hom.toOrderHom f.unop :
                    (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                  i))))
        j)
      (Functor.obj (Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
  (CategoryStruct.comp (Y := Functor.obj (classifyingSpaceUniversalCover G) X)
      (Iso.hom (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop X).len + 1)) ↦ G)) :
        Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
          (Functor.obj (classifyingSpaceUniversalCover G) X))
      (CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f ≫
          NatTrans.app
            (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))) j :
        Quiver.Hom (V := Action (Type u) G) (Functor.obj (classifyingSpaceUniversalCover G) X)
          (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j)) :
    Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
      (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
Tactic: rw [Category.assoc, limit.isoLimitCone_hom_π, limit.lift_π, Category.assoc]