-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y Z : PresheafedSpace.{v_1, u_1, u_3} C
f : X ⟶ Y
g : Y ⟶ Z
x :
  (↑(↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) : Type u_3)
w w₁ w₂ w₃ :
  Eq (α :=
    (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
      Type u_3))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
            { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F :
                { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.Hom
                  { carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } }.base :
          (a : (↑(↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F } : TopCat) : Type u_3)) →
            (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F } : TopCat) : Type u_3))
        x :
      (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
        Type u_3))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
            (X :=
            (↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat))
            (Y :=
            (↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat))
            (Hom.base
              ({ base := f.base, c := whiskerRight f.c F :
                  { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.Hom
                    { carrier := (↑Y : TopCat), presheaf := Y.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } } ≫
                { base := g.base, c := whiskerRight g.c F })) :
          (a : (↑(↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F } : TopCat) : Type u_3)) →
            (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F } : TopCat) : Type u_3))
        x :
      (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
        Type u_3))
⊢ Eq (α :=
    (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
      Type u_3))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
            { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F :
                { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.Hom
                  { carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } }.base :
          (a : (↑(↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F } : TopCat) : Type u_3)) →
            (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F } : TopCat) : Type u_3))
        x :
      (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
        Type u_3))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
            (X :=
            (↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat))
            (Y :=
            (↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat))
            (Hom.base
              ({ base := f.base, c := whiskerRight f.c F :
                  { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.Hom
                    { carrier := (↑Y : TopCat), presheaf := Y.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } } ≫
                { base := g.base, c := whiskerRight g.c F })) :
          (a : (↑(↑{ carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F } : TopCat) : Type u_3)) →
            (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F } : TopCat) : Type u_3))
        x :
      (↑(↑{ carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D } : TopCat) :
        Type u_3))

Tactic:
cat_disch