-- 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))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
s : Meq (FD := FD) (CD := CD) (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq (FD := FD) (CD := CD) P (T I)
ht : ∀ (I : S.Arrow), (↑s : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) I = mk (FD := FD) (CD := CD) (t I)
II : (S.bind T).Relation
a :
  Eq.{t + 1} (α := CD ((J.plusObj P).obj (op II.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map II.r.g₁.op) :
          (a : CD ((J.plusObj P).obj (op II.fst.Y))) → CD ((J.plusObj P).obj (op II.r.Z)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op II.fst.Y)) :
              (a : CD (P.obj (op II.fst.Y))) → CD ((J.plusObj P).obj (op II.fst.Y)))
            ((fun (I : (S.bind T).Arrow) ↦
                ((↑(t I.fromMiddle) : (I_1 : (T I.fromMiddle).Arrow) → ToType (P.obj (op I_1.Y))) I.toMiddle :
                  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.toMiddle.Y))))
              II.fst) :
          CD ((J.plusObj P).obj (op II.fst.Y))) :
      CD ((J.plusObj P).obj (op II.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map II.r.g₂.op) :
          (a : CD ((J.plusObj P).obj (op II.snd.Y))) → CD ((J.plusObj P).obj (op II.r.Z)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op II.snd.Y)) :
              (a : CD (P.obj (op II.snd.Y))) → CD ((J.plusObj P).obj (op II.snd.Y)))
            ((fun (I : (S.bind T).Arrow) ↦
                ((↑(t I.fromMiddle) : (I_1 : (T I.fromMiddle).Arrow) → ToType (P.obj (op I_1.Y))) I.toMiddle :
                  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.toMiddle.Y))))
              II.snd) :
          CD ((J.plusObj P).obj (op II.snd.Y))) :
      CD ((J.plusObj P).obj (op II.r.Z)))
⊢ Eq.{t + 1} (α := CD ((J.plusObj P).obj (op II.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op II.r.Z)) :
          (a : CD (P.obj (op II.r.Z))) → CD ((J.plusObj P).obj (op II.r.Z)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map II.r.g₁.op) :
              (a : CD (P.obj (op II.fst.Y))) → CD (P.obj (op II.r.Z)))
            ((fun (I : (S.bind T).Arrow) ↦
                ((↑(t I.fromMiddle) : (I_1 : (T I.fromMiddle).Arrow) → ToType (P.obj (op I_1.Y))) I.toMiddle :
                  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.toMiddle.Y))))
              II.fst) :
          CD (P.obj (op II.r.Z))) :
      CD ((J.plusObj P).obj (op II.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op II.r.Z)) :
          (a : CD (P.obj (op II.r.Z))) → CD ((J.plusObj P).obj (op II.r.Z)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map II.r.g₂.op) :
              (a : CD (P.obj (op II.snd.Y))) → CD (P.obj (op II.r.Z)))
            ((fun (I : (S.bind T).Arrow) ↦
                ((↑(t I.fromMiddle) : (I_1 : (T I.fromMiddle).Arrow) → ToType (P.obj (op I_1.Y))) I.toMiddle :
                  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.toMiddle.Y))))
              II.snd) :
          CD (P.obj (op II.r.Z))) :
      CD ((J.plusObj P).obj (op II.r.Z)))

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, (J.toPlus P).naturality,
      (J.toPlus P).naturality, ConcreteCategory.comp_apply, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.GrothendieckTopology.toPlus, CategoryTheory.NatTrans.naturality