-- 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ᵒᵖ
⊢ Eq (α :=
    F.obj (P.obj x) ⟶
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
    (CategoryStruct.comp (Y :=
        F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (F.map (Cover.toMultiequalizer ⊤ P) :
          F.obj (P.obj x) ⟶
            F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
          obj (C := (J.Cover (unop x))ᵒᵖ)
              ({ obj := fun (S : (J.Cover (unop x))ᵒᵖ) ↦ multiequalizer ((unop S).index P),
                  map := fun {S x_1 : (J.Cover (unop x))ᵒᵖ} (f : S ⟶ x_1) ↦
                    Multiequalizer.lift ((unop x_1).index P) (multiequalizer ((unop S).index P))
                      (fun (I : (unop x_1).shape.L) ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I f.unop)) ⋯,
                  map_id := ⋯, map_comp := ⋯ : (J.Cover (unop x))ᵒᵖ ⥤ D } ⋙
                F)
              (op ⊤) ⟶
            obj (C := (J.Cover (unop x))ᵒᵖ)
              { obj := fun (S : (J.Cover (unop x))ᵒᵖ) ↦ multiequalizer ((unop S).index (P ⋙ F)),
                map := fun {S x_1 : (J.Cover (unop x))ᵒᵖ} (f : S ⟶ x_1) ↦
                  Multiequalizer.lift ((unop x_1).index (P ⋙ F)) (multiequalizer ((unop S).index (P ⋙ F)))
                    (fun (I : (unop x_1).shape.L) ↦
                      Multiequalizer.ι ((unop S).index (P ⋙ F)) (Cover.Arrow.map I f.unop))
                    ⋯,
                map_id := ⋯, map_comp := ⋯ }
              (op ⊤)) :
      F.obj (P.obj x) ⟶
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
    (Cover.toMultiequalizer ⊤ (P ⋙ F) :
      (P ⋙ F).obj (op (unop x)) ⟶
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
have w : ∀ (a : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L),
  CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (CategoryStruct.comp (Y :=
          F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
          (F.map (Cover.toMultiequalizer ⊤ P) :
            F.obj (P.obj x) ⟶
              F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
          (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
            obj (C := (J.Cover (unop x))ᵒᵖ)
                ({ obj := fun (S : (J.Cover (unop x))ᵒᵖ) ↦ multiequalizer ((unop S).index P),
                    map := fun {S x_1 : (J.Cover (unop x))ᵒᵖ} (f : S ⟶ x_1) ↦
                      Multiequalizer.lift ((unop x_1).index P) (multiequalizer ((unop S).index P))
                        (fun (I : (unop x_1).shape.L) ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I f.unop))
                        sorry,
                    map_id := sorry, map_comp := sorry : (J.Cover (unop x))ᵒᵖ ⥤ D } ⋙
                  F)
                (op ⊤) ⟶
              obj (C := (J.Cover (unop x))ᵒᵖ)
                { obj := fun (S : (J.Cover (unop x))ᵒᵖ) ↦ multiequalizer ((unop S).index (P ⋙ F)),
                  map := fun {S x_1 : (J.Cover (unop x))ᵒᵖ} (f : S ⟶ x_1) ↦
                    Multiequalizer.lift ((unop x_1).index (P ⋙ F)) (multiequalizer ((unop S).index (P ⋙ F)))
                      (fun (I : (unop x_1).shape.L) ↦
                        Multiequalizer.ι ((unop S).index (P ⋙ F)) (Cover.Arrow.map I f.unop))
                      sorry,
                  map_id := sorry, map_comp := sorry : (J.Cover (unop x))ᵒᵖ ⥤ E }
                (op ⊤)) :
        F.obj (P.obj x) ⟶
          multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (Multiequalizer.ι (Cover.index ⊤ (P ⋙ F)) a :
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)) ⟶
          MulticospanIndex.left (Cover.index ⊤ (P ⋙ F)) a) =
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (Cover.toMultiequalizer ⊤ (P ⋙ F)) (Multiequalizer.ι (Cover.index ⊤ (P ⋙ F)) a)
Tactic: ext a