-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Eq (α := multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))
    (Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
          (fun (x : (unop j).Arrow) ↦
            Multiequalizer.ι ((unop j).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
          ⋯ ≫
        colimit.ι (J.diagram (F.obj k) X) j :
      multiequalizer ((unop j).index (limit F)) ⟶ colimit (J.diagram (F.obj k) X))
    (CategoryStruct.comp (Y := (limit (F ⋙ J.diagramFunctor D X)).obj j)
        (NatTrans.app (limit.lift (F ⋙ J.diagramFunctor D X) (Functor.mapCone (J.diagramFunctor D X) (limit.cone F))) j)
        (NatTrans.app (limit.π (F ⋙ J.diagramFunctor D X) k) j ≫
          CategoryStruct.comp (Y := (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
            (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
              ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
            (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
              (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ⟶ (J.plusObj (F.obj k)).obj (op X))) :
      multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))
have e_a : Eq (α := multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))
  (Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun (x : (unop j).Arrow) ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
        sorry ≫
      colimit.ι (J.diagram (F.obj k) X) j :
    multiequalizer ((unop j).index (limit F)) ⟶ colimit (J.diagram (F.obj k) X))
  (CategoryStruct.comp (Y := (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
      (NatTrans.app
            (CategoryStruct.comp (Y := limit (F ⋙ J.diagramFunctor D X))
              (limit.lift (F ⋙ J.diagramFunctor D X) (Functor.mapCone (J.diagramFunctor D X) (limit.cone F)))
              (limit.π (F ⋙ J.diagramFunctor D X) k))
            j ≫
          NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
        multiequalizer ((unop j).index (limit F)) ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
      (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
        (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ⟶ (J.plusObj (F.obj k)).obj (op X)) :
    multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))
Tactic: simp_rw [← Category.assoc, ← NatTrans.comp_app]