-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
    (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
        (F.map (colimit.ι (J.diagram P (unop X)) W) :
          F.obj (obj (J.diagram P (unop X)) W) ⟶ F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
        (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : Cᵒᵖ) ↦
                  Iso.trans (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
                    (IsColimit.coconePointUniqueUpToIso
                      (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
                      (colimit.isColimit (J.diagram P (unop X) ⋙ F)))
                    (HasColimit.isoOfNatIso
                      (NatIso.ofComponents
                        (fun (W : (J.Cover (unop X))ᵒᵖ) ↦
                          Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                            (IsLimit.conePointUniqueUpToIso
                              (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                              (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                            (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm))
                        ⋯)))
                ⋯))
            X :
          (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ F)).obj X) :
      F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
    (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ F) (unop X)) W)
        (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (W : (J.Cover (unop X))ᵒᵖ) ↦
                  Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                    (IsLimit.conePointUniqueUpToIso
                      (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                      (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                    (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm))
                ⋯))
            W :
          obj (J.diagram P (unop X) ⋙ F) W ⟶ obj (J.diagram (P ⋙ F) (unop X)) W)
        (colimit.ι (J.diagram (P ⋙ F) (unop X)) W :
          obj (J.diagram (P ⋙ F) (unop X)) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X))) :
      obj (J.diagram P (unop X) ⋙ F) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
have simp : Eq (α := F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
  (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
      (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
        (F.map (colimit.ι (J.diagram P (unop X)) W))
        (Iso.hom
          (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
            (colimit.isColimit (J.diagram P (unop X) ⋙ F)))))
      (Iso.hom
        (HasColimit.isoOfNatIso
          (NatIso.ofComponents
            (fun (W : (J.Cover (unop X))ᵒᵖ) ↦
              Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                  (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm))
            sorry))) :
    F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
  (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ F) (unop X)) W)
      (CategoryStruct.comp (Y := limit (((unop W).index P).multicospan ⋙ F))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
            (limit.isLimit (((unop W).index P).multicospan ⋙ F))))
        (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)))
      (colimit.ι (J.diagram (P ⋙ F) (unop X)) W) :
    obj (J.diagram P (unop X) ⋙ F) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))
Tactic: simp only [Iso.trans_hom, NatIso.ofComponents_hom_app, ←
    Category.assoc]