-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
e : x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
h :
  ∀ (t : (unop (op S)).shape.L),
    Eq.{t + 1} (α := CD (((unop (op S)).index P).left t))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι ((unop (op S)).index P) t) :
            (a : CD (multiequalizer ((unop (op S)).index P))) → CD (((unop (op S)).index P).left t))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1.op) :
                (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj (op S)))
              ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                    (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
                  x :
                ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
            CD ((J.diagram P X).obj (op S))) :
        CD (((unop (op S)).index P).left t))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι ((unop (op S)).index P) t) :
            (a : CD (multiequalizer ((unop (op S)).index P))) → CD (((unop (op S)).index P).left t))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2.op) :
                (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj (op S)))
              ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P)))
                  y :
                ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
            CD ((J.diagram P X).obj (op S))) :
        CD (((unop (op S)).index P).left t))
⊢ Eq.{t + 1} (α := CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1.op) :
          (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) : (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
            x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
      CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2.op) :
          (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
      CD ((J.diagram P X).obj (op S)))

Tactic:
apply Concrete.multiequalizer_ext

Premises used: CategoryTheory.Limits.Concrete.multiequalizer_ext