-- 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
w :
  ∀
    (x :
      (↑(↑{ carrier := (↑X : TopCat), presheaf := X.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))
h :
  ∀
    (U :
      Opens
        (↑(↑{ 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 }.presheaf.obj (op U) ⟶
        obj
          (Functor.op
              (Opens.map
                (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 :
                      { carrier := (↑Y : TopCat), presheaf := Y.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 } }))) ⋙
            { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf)
          (op U))
      (NatTrans.app
          (CategoryStruct.comp (Y :=
            obj
              (Presheaf.pushforward D
                { 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)
              { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf)
            { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.c
            (whiskerRight (eqToHom ⋯) { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F }.presheaf))
          (op U) :
        { carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf.obj
            (op U) ⟶
          obj
            (Functor.op
                (Opens.map
                  (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 :
                        { carrier := (↑Y : TopCat), presheaf := Y.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 } }))) ⋙
              { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf)
            (op U))
      (NatTrans.app
          (Hom.c
            ({ 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 }))
          (op U) :
        { carrier := (↑Z : TopCat), presheaf := Z.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf.obj
            (op U) ⟶
          obj
            (Functor.op
                (Opens.map
                  (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 :
                        { carrier := (↑Y : TopCat), presheaf := Y.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 } }))) ⋙
              { carrier := (↑X : TopCat), presheaf := X.presheaf ⋙ F : PresheafedSpace.{v_2, u_2, u_3} D }.presheaf)
            (op U))
⊢ { 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 := 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 }

Tactic:
ext