-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
h :
  ∀ (t : S.shape.L),
    Eq (α := CD ((S.index P).left t))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) t) :
            (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left t))
          ((ConcreteCategory.hom (FC := FD) (CC := CD)
                  (Multiequalizer.lift (S.index P)
                    (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
                    (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) ⋯) :
                (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
              ((ConcreteCategory.hom (FC := FD) (CC := CD)
                      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                        (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) ⋯) :
                    (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                  x :
                CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
            CD (multiequalizer (S.index P))) :
        CD ((S.index P).left t))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) t) :
            (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left t))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
              (Meq.mk (FD := FD) (CD := CD) S x) :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
        CD ((S.index P).left t))
⊢ Eq (α := CD (multiequalizer (S.index P)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift (S.index P)
              (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
              (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) ⋯) :
          (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                  (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) ⋯) :
              (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
            x :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD (multiequalizer (S.index P)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
        (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))

Tactic:
apply Concrete.multiequalizer_ext (C := D)

Premises used: CategoryTheory.Limits.Concrete.multiequalizer_ext