-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
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 :
  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))
⊢ ℱ.map
      (CommaMorphism.left
        (IsTerminal.from
          {
            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 := ⋯ }
          (obj (CostructuredArrow.map (homOfLE le).op) j))) =
    ℱ.map
        (IsTerminal.from
            {
              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 := ⋯ :
              IsLimit (C := CostructuredArrow (Opens.map f).op (op V))
                (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)) ''
                            (↑V : Set (↑X : Type v)),
                        is_open' := HV : Opens (↑Y : Type v) })
                    (homOfLE ⋯).op)) }
            j).left ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op
have rw : ℱ.map
    (CommaMorphism.left
      (IsTerminal.from
        {
          lift :=
            fun
              (s :
                Cone (C := CostructuredArrow (Opens.map f).op (op U))
                  (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
            CostructuredArrow.homMk (homOfLE sorry).op sorry,
          fac := sorry, uniq := sorry }
        (obj (CostructuredArrow.map (homOfLE le).op) j))) =
  ℱ.map
    ((IsTerminal.from
          {
            lift :=
              fun
                (s :
                  Cone (C := CostructuredArrow (Opens.map f).op (op V))
                    (empty (CostructuredArrow (Opens.map f).op (op V)))) ↦
              CostructuredArrow.homMk (homOfLE sorry).op sorry,
            fac := sorry, uniq := sorry :
            IsLimit (C := CostructuredArrow (Opens.map f).op (op V))
              (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)) ''
                          (↑V : Set (↑X : Type v)),
                      is_open' := HV : Opens (↑Y : Type v) })
                  (homOfLE sorry).op)) }
          j).left ≫
      (IsOpenMap.functorMap HU HV le).op)
Tactic: rw [← Functor.map_comp]