-- Module: Mathlib.RepresentationTheory.Homological.Resolution
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))
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))
⊢ 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))

Tactic:
rw [Category.assoc, limit.isoLimitCone_hom_π, limit.lift_π, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Limits.limit.lift_π