-- 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
⊢ 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)
have 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))
Tactic: refine IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => ?_