-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a : ((unop W).pullback f.unop).shape.L
e_a :
  Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
      (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) :
        F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
      (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index (P ⋙ F)))
          (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop Y))) (op ((unop W).pullback f.unop)) :
            obj (J.diagram P (unop Y) ⋙ F) (op ((unop W).pullback f.unop)) ⟶
              obj (J.diagram (P ⋙ F) (unop Y)) (op ((unop W).pullback f.unop)))
          (Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a :
            multiequalizer (((unop W).pullback f.unop).index (P ⋙ F)) ⟶
              (((unop W).pullback f.unop).index (P ⋙ F)).left a) :
        F.obj (multiequalizer (((unop W).pullback f.unop).index P)) ⟶ F.obj (P.obj (op a.Y))))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
      (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.ι ((unop W).index (P ⋙ F)) (Cover.Arrow.base a) :
        multiequalizer ((unop W).index (P ⋙ F)) ⟶ ((unop W).index (P ⋙ F)).left (Cover.Arrow.base a)))
e_a₁ :
  Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
      (F.map
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯))
      (F.map (Multiequalizer.ι ((unop (op ((unop W).pullback f.unop))).index P) a)))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
      (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.ι ((unop W).index (P ⋙ F)) (Cover.Arrow.base a) :
        multiequalizer ((unop W).index (P ⋙ F)) ⟶ ((unop W).index (P ⋙ F)).left (Cover.Arrow.base a)))
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
        (F.map
            (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
              (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) :
          F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
        (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index (P ⋙ F)))
            (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop Y))) (op ((unop W).pullback f.unop)) :
              obj (J.diagram P (unop Y) ⋙ F) (op ((unop W).pullback f.unop)) ⟶
                obj (J.diagram (P ⋙ F) (unop Y)) (op ((unop W).pullback f.unop)))
            (Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a :
              multiequalizer (((unop W).pullback f.unop).index (P ⋙ F)) ⟶
                (((unop W).pullback f.unop).index (P ⋙ F)).left a) :
          F.obj (multiequalizer (((unop W).pullback f.unop).index P)) ⟶ F.obj (P.obj (op a.Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
    (CategoryStruct.comp (Y := multiequalizer ((unop W).index (P ⋙ F)))
        (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 := multiequalizer (((unop W).pullback f.unop).index (P ⋙ F)))
            (Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
              (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯)
            (Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a) :
          multiequalizer ((unop W).index (P ⋙ F)) ⟶ F.obj (P.obj (op a.Y))) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
have e_a₂ : Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (P.obj (op a.Y)))
  (CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
    (F.map
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry))
    (F.map (Multiequalizer.ι ((unop (op ((unop W).pullback f.unop))).index P) a)))
  (F.map (Multiequalizer.ι ((unop W).index P) (Cover.Arrow.base a)))
Tactic: rw [Multiequalizer.lift_ι, diagramCompIso_hom_ι, diagramCompIso_hom_ι, ← F.map_comp,
        Multiequalizer.lift_ι]