-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
refine :
  ∀ (j : Discrete (Fin ((Opposite.unop Y).len + 1))),
    Eq (α :=
      Quiver.Hom (V := Action (Type u) G) (Functor.obj (cechNerveTerminalFrom (Action.ofMulAction G G)) X)
        (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)))
        (CategoryTheory.Functor.map (cechNerveTerminalFrom (Action.ofMulAction G G)) f ≫
            Iso.hom
              ((fun (x : SimplexCategoryᵒᵖ) ↦
                  (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
                    Iso (C := Action (Type u) G)
                      (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                        (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                      (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                        Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                        (LimitCone.cone
                          (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
                Y) :
          Quiver.Hom (V := Action (Type u) G) (Functor.obj (cechNerveTerminalFrom (Action.ofMulAction G G)) X)
            (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)))
      (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)))
        (Iso.hom
              ((fun (x : SimplexCategoryᵒᵖ) ↦
                  (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
                    Iso (C := Action (Type u) G)
                      (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                        (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                      (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                        Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                        (LimitCone.cone
                          (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
                X) ≫
            CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f :
          Quiver.Hom (V := Action (Type u) G) (Functor.obj (cechNerveTerminalFrom (Action.ofMulAction G G)) X)
            (Functor.obj (classifyingSpaceUniversalCover G) Y))
        (NatTrans.app
          (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G))) j))
⊢ Eq (α :=
    Quiver.Hom (V := Action (Type u) G) (Functor.obj (cechNerveTerminalFrom (Action.ofMulAction G G)) X)
      (Functor.obj (classifyingSpaceUniversalCover G) Y))
    (CategoryTheory.Functor.map (cechNerveTerminalFrom (Action.ofMulAction G G)) f ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
              Iso (C := Action (Type u) G)
                (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                  (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
          Y))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
              Iso (C := Action (Type u) G)
                (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                  (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
          X) ≫
      CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f)

Tactic:
refine IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => ?_