-- 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
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
⊢ Eq (α := F.obj (multiequalizer ((unop A).index P)) ⟶ multiequalizer ((unop B).index (P ⋙ F)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop B).index P)))
      (F.map
        (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
          (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) ⋯))
      (CategoryStruct.comp (Y := limit (((unop B).index P).multicospan ⋙ F))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan))
            (limit.isLimit (((unop B).index P).multicospan ⋙ F))))
        (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm))))
    (CategoryStruct.comp (Y := multiequalizer ((unop A).index (P ⋙ F)))
      (CategoryStruct.comp (Y := limit (((unop A).index P).multicospan ⋙ F))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan))
            (limit.isLimit (((unop A).index P).multicospan ⋙ F))))
        (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm)))
      (Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
        (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) ⋯))
have h : ∀ (g : (unop B).shape.L),
  Eq (α := F.obj (multiequalizer ((unop A).index P)) ⟶ ((unop B).index (P ⋙ F)).left g)
    (CategoryStruct.comp (Y := multiequalizer ((unop B).index (P ⋙ F)))
      (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop B).index P)))
        (F.map
          (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
            (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) sorry))
        (CategoryStruct.comp (Y := limit (((unop B).index P).multicospan ⋙ F))
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan))
              (limit.isLimit (((unop B).index P).multicospan ⋙ F))))
          (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm))))
      (Multiequalizer.ι ((unop B).index (P ⋙ F)) g))
    (CategoryStruct.comp (Y := multiequalizer ((unop B).index (P ⋙ F)))
      (CategoryStruct.comp (Y := multiequalizer ((unop A).index (P ⋙ F)))
        (CategoryStruct.comp (Y := limit (((unop A).index P).multicospan ⋙ F))
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan))
              (limit.isLimit (((unop A).index P).multicospan ⋙ F))))
          (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm)))
        (Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
          (fun (I : (unop B).Arrow) ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) sorry))
      (Multiequalizer.ι ((unop B).index (P ⋙ F)) g))
Tactic: ext g