-- 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 : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
rw :
  Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))) :
          (a : CD ((J.diagram P I.Y).obj (op ((J.pullback I.f).obj (unop (op S)))))) → CD (colimit (J.diagram P I.Y)))
        (((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (Functor.map (J.diagram P I.Y) e.op) :
                FD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
                  (Functor.obj (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S)))))) :
              (a : CD (multiequalizer (⊤.index P))) →
                CD ((J.diagram P I.Y).obj (op ((J.pullback I.f).obj (unop (op S))))))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op I.Y))
                      (fun (I_1 : Cover.Arrow.{v, u} (C := C) (X := I.Y) (J := J) ⊤) ↦ P.map I_1.f.op) ⋯) :
                  (a : CD (P.obj (op I.Y))) → CD (multiequalizer (⊤.index P)))
                ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD (Functor.obj (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S)))))) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    (((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _
              (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) :
            FD
              (Functor.obj
                (Functor.comp (D := (J.Cover I.Y)ᵒᵖ)
                  { obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                    map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op, map_id := ⋯,
                    map_comp := ⋯ }
                  (J.diagram P I.Y))
                (op S))
              (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y))) :
          (a :
              CD
                (({ obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                        map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op,
                        map_id := ⋯, map_comp := ⋯ } ⋙
                      J.diagram P I.Y).obj
                  (op S))) →
            CD (colimit (J.diagram P I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P I.f) (op S)) :
              (a : CD (multiequalizer (S.index P))) →
                CD
                  (({ obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                          map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op,
                          map_id := ⋯, map_comp := ⋯ } ⋙
                        J.diagram P I.Y).obj
                    (op S)))
            ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
                x :
              ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
          CD
            (Functor.obj
              (Functor.comp (D := (J.Cover I.Y)ᵒᵖ)
                { obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                  map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op, map_id := ⋯,
                  map_comp := ⋯ }
                (J.diagram P I.Y))
              (op S))) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
⊢ Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    (((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (colimit.ι (J.diagram P I.Y) (op ⊤)) :
            FD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
              (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y))) :
          (a : CD (multiequalizer (⊤.index P))) → CD (colimit (J.diagram P I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op I.Y))
                  (fun (I_1 : Cover.Arrow.{v, u} (C := C) (X := I.Y) (J := J) ⊤) ↦ P.map I_1.f.op) ⋯) :
              (a : CD (P.obj (op I.Y))) → CD (multiequalizer (⊤.index P)))
            ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    (((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _
              (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) :
            FD
              (Functor.obj
                (Functor.comp (D := (J.Cover I.Y)ᵒᵖ)
                  { obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                    map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op, map_id := ⋯,
                    map_comp := ⋯ }
                  (J.diagram P I.Y))
                (op S))
              (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y))) :
          (a :
              CD
                (({ obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                        map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op,
                        map_id := ⋯, map_comp := ⋯ } ⋙
                      J.diagram P I.Y).obj
                  (op S))) →
            CD (colimit (J.diagram P I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P I.f) (op S)) :
              (a : CD (multiequalizer (S.index P))) →
                CD
                  (({ obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                          map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op,
                          map_id := ⋯, map_comp := ⋯ } ⋙
                        J.diagram P I.Y).obj
                    (op S)))
            ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
                x :
              ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
          CD
            (Functor.obj
              (Functor.comp (D := (J.Cover I.Y)ᵒᵖ)
                { obj := fun (X_1 : (J.Cover X)ᵒᵖ) ↦ op ((J.pullback I.f).obj (unop X_1)),
                  map := fun {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y) ↦ ((J.pullback I.f).map f.unop).op, map_id := ⋯,
                  map_comp := ⋯ }
                (J.diagram P I.Y))
              (op S))) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))

Tactic:
rw [← colimit.w _ e.op, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, Quiver.Hom.op, CategoryTheory.Limits.colimit.w