-- 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
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
    (η.app (multiequalizer ((unop W).index P)) ≫
        CategoryStruct.comp (Y := obj (J.diagram (P ⋙ G) (unop X)) W)
          (NatTrans.app (Iso.hom (J.diagramCompIso G P (unop X))) W :
            obj (J.diagram P (unop X) ⋙ G) W ⟶ obj (J.diagram (P ⋙ G) (unop X)) W)
          (colimit.ι (J.diagram (P ⋙ G) (unop X)) W :
            obj (J.diagram (P ⋙ G) (unop X)) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
    (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ F) (unop X)) W)
        (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
          obj (J.diagram P (unop X) ⋙ F) W ⟶ obj (J.diagram (P ⋙ F) (unop X)) W)
        (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ G) (unop X)) W)
            (Multiequalizer.lift ((unop W).index (P ⋙ G)) (obj (J.diagram (P ⋙ F) (unop X)) W)
              (fun (x : (unop W).shape.L) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ η.app (P.obj (op x.Y))) ⋯)
            (colimit.ι (J.diagram (P ⋙ G) (unop X)) W) :
          obj (J.diagram (P ⋙ F) (unop X)) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
      F.obj (obj (J.diagram P (unop X)) W) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
have w : Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
  (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ G) (unop X)) W)
      (η.app (multiequalizer ((unop W).index P)) ≫ NatTrans.app (Iso.hom (J.diagramCompIso G P (unop X))) W :
        F.obj (multiequalizer ((unop W).index P)) ⟶ obj (J.diagram (P ⋙ G) (unop X)) W)
      (colimit.ι (J.diagram (P ⋙ G) (unop X)) W :
        obj (J.diagram (P ⋙ G) (unop X)) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
  (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ G) (unop X)) W)
      (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ F) (unop X)) W)
        (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
          obj (J.diagram P (unop X) ⋙ F) W ⟶ obj (J.diagram (P ⋙ F) (unop X)) W)
        (Multiequalizer.lift ((unop W).index (P ⋙ G)) (obj (J.diagram (P ⋙ F) (unop X)) W)
            (fun (x : (unop W).shape.L) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ η.app (P.obj (op x.Y))) sorry :
          obj (J.diagram (P ⋙ F) (unop X)) W ⟶ multiequalizer ((unop W).index (P ⋙ G))))
      (colimit.ι (J.diagram (P ⋙ G) (unop X)) W) :
    F.obj (obj (J.diagram P (unop X)) W) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ G) (unop X)))
Tactic: simp only [← Category.assoc]