-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)
        (NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)))
          j)
        (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U)) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)))
          j :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)
⊢ Eq (α := ℱ.obj j.left ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (u.app j.left ≫
      𝒢.map
        (CommaMorphism.left
          (Limits.IsTerminal.from
            {
              lift :=
                fun
                  (s :
                    Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            j)))
    (ℱ.map
        (CommaMorphism.left
          (Limits.IsTerminal.from
            {
              lift :=
                fun
                  (s :
                    Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            j)) ≫
      u.app (op (hf.functor.obj U)))
have w : Eq (α := ℱ.obj j.left ⟶ 𝒢.obj (op (hf.functor.obj U)))
  (ℱ.map
      (CommaMorphism.left
        (Limits.IsTerminal.from
          {
            lift :=
              fun
                (s :
                  Limits.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 }
          j)) ≫
    u.app
      (op
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type v)) → (↑Y : Type v)) ''
              (↑U : Set (↑X : Type v)),
          is_open' := sorry : Opens (↑Y : Type v) }))
  (ℱ.map
      (CommaMorphism.left
        (Limits.IsTerminal.from
          {
            lift :=
              fun
                (s :
                  Limits.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 }
          j)) ≫
    u.app (op (hf.functor.obj U)))
Tactic: rw [← u.naturality]