-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
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
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
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
w :
  ∀ (a : (unop W).shape.L),
    Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ ((unop W).index (Q ⋙ F)).left a)
      (CategoryStruct.comp (Y := multiequalizer ((unop W).index (Q ⋙ F)))
          (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop W).index Q)))
              (F.map
                  (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
                    (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) :
                F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (multiequalizer ((unop W).index Q)))
              (NatTrans.app (Iso.hom (J.diagramCompIso F Q (unop X))) W :
                obj
                    ({ obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index Q),
                        map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                          Multiequalizer.lift ((unop x).index Q) (multiequalizer ((unop S).index Q))
                            (fun (I : (unop x).shape.L) ↦
                              Multiequalizer.ι ((unop S).index Q) (Cover.Arrow.map I f.unop))
                            ⋯,
                        map_id := ⋯, map_comp := ⋯ : (J.Cover (unop X))ᵒᵖ ⥤ D } ⋙
                      F)
                    W ⟶
                  obj
                    { obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index (Q ⋙ F)),
                      map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                        Multiequalizer.lift ((unop x).index (Q ⋙ F)) (multiequalizer ((unop S).index (Q ⋙ F)))
                          (fun (I : (unop x).shape.L) ↦
                            Multiequalizer.ι ((unop S).index (Q ⋙ F)) (Cover.Arrow.map I f.unop))
                          ⋯,
                      map_id := ⋯, map_comp := ⋯ }
                    W) :
            F.obj (multiequalizer ((unop W).index P)) ⟶ multiequalizer ((unop W).index (Q ⋙ F)))
          (Multiequalizer.ι ((unop W).index (Q ⋙ F)) a :
            multiequalizer ((unop W).index (Q ⋙ F)) ⟶ ((unop W).index (Q ⋙ F)).left a) :
        F.obj (multiequalizer ((unop W).index P)) ⟶ ((unop W).index (Q ⋙ F)).left a)
      (CategoryStruct.comp (Y := multiequalizer ((unop W).index (Q ⋙ F)))
          (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
            (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
              obj
                  ({ obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index P),
                      map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                        Multiequalizer.lift ((unop x).index P) (multiequalizer ((unop S).index P))
                          (fun (I : (unop x).shape.L) ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I f.unop))
                          ⋯,
                      map_id := ⋯, map_comp := ⋯ : (J.Cover (unop X))ᵒᵖ ⥤ D } ⋙
                    F)
                  W ⟶
                obj
                  { obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index (P ⋙ F)),
                    map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                      Multiequalizer.lift ((unop x).index (P ⋙ F)) (multiequalizer ((unop S).index (P ⋙ F)))
                        (fun (I : (unop x).shape.L) ↦
                          Multiequalizer.ι ((unop S).index (P ⋙ F)) (Cover.Arrow.map I f.unop))
                        ⋯,
                    map_id := ⋯, map_comp := ⋯ }
                  W)
            (Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
                (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯ :
              multiequalizer ((unop W).index (P ⋙ F)) ⟶ multiequalizer ((unop W).index (Q ⋙ F))))
          (Multiequalizer.ι ((unop W).index (Q ⋙ F)) a) :
        F.obj (multiequalizer ((unop W).index P)) ⟶ ((unop W).index (Q ⋙ F)).left a)
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ multiequalizer ((unop W).index (Q ⋙ F)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop W).index Q)))
        (F.map
            (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
              (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) :
          F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (multiequalizer ((unop W).index Q)))
        (NatTrans.app (Iso.hom (J.diagramCompIso F Q (unop X))) W :
          obj
              ({ obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index Q),
                  map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                    Multiequalizer.lift ((unop x).index Q) (multiequalizer ((unop S).index Q))
                      (fun (I : (unop x).shape.L) ↦ Multiequalizer.ι ((unop S).index Q) (Cover.Arrow.map I f.unop)) ⋯,
                  map_id := ⋯, map_comp := ⋯ : (J.Cover (unop X))ᵒᵖ ⥤ D } ⋙
                F)
              W ⟶
            obj
              { obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index (Q ⋙ F)),
                map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                  Multiequalizer.lift ((unop x).index (Q ⋙ F)) (multiequalizer ((unop S).index (Q ⋙ F)))
                    (fun (I : (unop x).shape.L) ↦ Multiequalizer.ι ((unop S).index (Q ⋙ F)) (Cover.Arrow.map I f.unop))
                    ⋯,
                map_id := ⋯, map_comp := ⋯ }
              W) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ multiequalizer ((unop W).index (Q ⋙ F)))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
        (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop X))) W :
          obj
              ({ obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index P),
                  map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                    Multiequalizer.lift ((unop x).index P) (multiequalizer ((unop S).index P))
                      (fun (I : (unop x).shape.L) ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I f.unop)) ⋯,
                  map_id := ⋯, map_comp := ⋯ : (J.Cover (unop X))ᵒᵖ ⥤ D } ⋙
                F)
              W ⟶
            obj
              { obj := fun (S : (J.Cover (unop X))ᵒᵖ) ↦ multiequalizer ((unop S).index (P ⋙ F)),
                map := fun {S x : (J.Cover (unop X))ᵒᵖ} (f : S ⟶ x) ↦
                  Multiequalizer.lift ((unop x).index (P ⋙ F)) (multiequalizer ((unop S).index (P ⋙ F)))
                    (fun (I : (unop x).shape.L) ↦ Multiequalizer.ι ((unop S).index (P ⋙ F)) (Cover.Arrow.map I f.unop))
                    ⋯,
                map_id := ⋯, map_comp := ⋯ }
              W)
        (Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
            (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯ :
          multiequalizer ((unop W).index (P ⋙ F)) ⟶ multiequalizer ((unop W).index (Q ⋙ F))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ multiequalizer ((unop W).index (Q ⋙ F)))

Tactic:
ext a