-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens (↑X : Type v)
HU :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
HV :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑V : Set (↑X : Type v)))
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
⊢ Eq (α :=
    obj (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ) j ⟶
      ℱ.obj
        (op
          {
            carrier :=
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      f) :
                  (a : (↑X : Type v)) → (↑Y : Type v)) ''
                (↑U : Set (↑X : Type v)),
            is_open' := HU }))
    (NatTrans.app
        (Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op V)))
        j ≫
      (obj (pullback C f) ℱ).map (homOfLE le).op ≫
        Iso.hom
          (IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (colimitOfDiagramTerminal
              {
                lift :=
                  fun
                    (s :
                      Cone (C := CostructuredArrow (Opens.map f).op (op U))
                        (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ :
                IsLimit (C := CostructuredArrow (Opens.map f).op (op U))
                  (asEmptyCone
                    (CostructuredArrow.mk (Y :=
                      op
                        {
                          carrier :=
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
                                    (CC := carrier) f) :
                                (a : (↑X : Type v)) → (↑Y : Type v)) ''
                              (↑U : Set (↑X : Type v)),
                          is_open' := HU : Opens (↑Y : Type v) })
                      (homOfLE ⋯).op)) }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))))
    (CategoryStruct.comp (Y :=
      obj
        (obj (Functor.const (CostructuredArrow (Opens.map f).op (op V)))
          (Cocone.pt (J := CostructuredArrow (Opens.map f).op (op V))
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V))))
        j)
      (NatTrans.app
        (Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op V)))
        j)
      (Iso.hom
          (IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
            (colimitOfDiagramTerminal
              {
                lift :=
                  fun
                    (s :
                      Cone (C := CostructuredArrow (Opens.map f).op (op V))
                        (empty (CostructuredArrow (Opens.map f).op (op V)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))) ≫
        ℱ.map (IsOpenMap.functorMap HU HV le).op))
have eq : Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ) j ⟶ (obj (pullback C f) ℱ).obj (op U))
  (NatTrans.app
        (Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op V)))
        j ≫
      (obj (pullback C f) ℱ).map (homOfLE le).op :
    obj (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ) j ⟶ (obj (pullback C f) ℱ).obj (op U))
  (NatTrans.app
      (Cocone.ι
        ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
          (op U)))
      (obj (CostructuredArrow.map (homOfLE le).op) j) :
    obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) (obj (CostructuredArrow.map (homOfLE le).op) j) ⟶
      obj
        (obj (Functor.const (CostructuredArrow (Opens.map f).op (op U)))
          (Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U))))
        (obj (CostructuredArrow.map (homOfLE le).op) j))
Tactic: have eq : ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op V)).ι.app j ≫ ((pullback C f).obj ℱ).map (homOfLE le).op =
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op U)).ι.app ((CostructuredArrow.map (homOfLE le).op).obj j) := by cat_disch