-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop : Opens (↑(↑Z : TopCat) : Type u_1)
⊢ Eq (α :=
    Z.presheaf.obj (op unop) ⟶
      (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
        (op unop))
    (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj
            (TopCat.Presheaf.pushforward C (Hom.base (pullbackConeOfLeftFst f g ≫ f)) :
              TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⥤
                TopCat.Presheaf.{u_1, v, u} C (↑Z : TopCat))
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf)
          (Hom.c (pullbackConeOfLeftFst f g ≫ f) :
            Z.presheaf ⟶
              Functor.obj
                (TopCat.Presheaf.pushforward C (Hom.base (pullbackConeOfLeftFst f g ≫ f)) :
                  TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⥤
                    TopCat.Presheaf.{u_1, v, u} C (↑Z : TopCat))
                (Y.restrict (U := pullback f.base g.base) ⋯).presheaf)
          (Functor.whiskerRight (eqToHom ⋯) (Y.restrict (U := pullback f.base g.base) ⋯).presheaf :
            Functor.op (Opens.map (Hom.base (pullbackConeOfLeftFst f g ≫ f))) ⋙
                (Y.restrict (U := pullback f.base g.base) ⋯).presheaf ⟶
              Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
                (Y.restrict (U := pullback f.base g.base) ⋯).presheaf))
        (op unop) :
      Z.presheaf.obj (op unop) ⟶
        (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
          (op unop))
    (NatTrans.app (Hom.c (Y.ofRestrict ⋯ ≫ g)) (op unop) :
      Z.presheaf.obj (op unop) ⟶
        (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
          (op unop))
have refine_2 : Eq (α :=
  Z.presheaf.obj (op unop) ⟶
    Y.presheaf.obj
      (op
        (Functor.obj (IsOpenEmbedding.functor sorry)
          (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop)))))
  (g.c.app (op unop) ≫
      CategoryStruct.comp (Y :=
        Y.presheaf.obj (op ((Opens.map g.base).obj ((opensFunctor f).obj ((Opens.map f.base).obj unop)))))
        (Y.presheaf.map
            (Quiver.Hom.op
              ((Opens.map g.base).map
                (Quiver.Hom.unop
                  (Quiver.Hom.op (X :=
                    Set.image (α := (↑(↑X : TopCat) : Type u_1))
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                            (CC := TopCat.carrier) f.base) :
                        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                              (CC := TopCat.carrier) f.base) :
                          (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
                        (↑unop : Set (↑(↑Z : TopCat) : Type u_1))))
                    (Y := (↑unop : Set (↑(↑Z : TopCat) : Type u_1)))
                    (homOfLE (x :=
                      Set.image (α := (↑(↑X : TopCat) : Type u_1))
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                              (CC := TopCat.carrier) f.base) :
                          (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
                        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                                (CC := TopCat.carrier) f.base) :
                            (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
                          (↑unop : Set (↑(↑Z : TopCat) : Type u_1))))
                      (y := (↑unop : Set (↑(↑Z : TopCat) : Type u_1))) sorry))))) :
          Y.presheaf.obj (op ((Opens.map g.base).obj unop)) ⟶
            Y.presheaf.obj (op ((Opens.map g.base).obj ((opensFunctor f).obj ((Opens.map f.base).obj unop)))))
        (CategoryStruct.comp (Y :=
            Y.presheaf.obj
              (op
                (Functor.obj (IsOpenEmbedding.functor sorry)
                  (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop)))))
            (Y.presheaf.map (eqToHom sorry) :
              Y.presheaf.obj
                  (op
                    ((Opens.map g.base).obj
                      (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) ((Opens.map f.base).obj unop)))) ⟶
                Y.presheaf.obj
                  (op
                    (sorry.functor.obj
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop)))))
            (Y.presheaf.map (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor sorry) (eqToHom sorry))) :
              Y.presheaf.obj
                  (op
                    (Functor.obj (IsOpenEmbedding.functor sorry)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop)))) ⟶
                Y.presheaf.obj
                  (op
                    (Functor.obj (IsOpenEmbedding.functor sorry)
                      (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop))))) :
          Y.presheaf.obj (op ((Opens.map g.base).obj ((opensFunctor f).obj ((Opens.map f.base).obj unop)))) ⟶
            Y.presheaf.obj
              (op
                (Functor.obj (IsOpenEmbedding.functor sorry)
                  (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop))))) :
    Z.presheaf.obj (op unop) ⟶
      Y.presheaf.obj
        (op
          (Functor.obj (IsOpenEmbedding.functor sorry)
            (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop)))))
  (g.c.app (op unop) ≫
      Y.presheaf.map
        (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction sorry)) ((Opens.map g.base).obj unop))) :
    Z.presheaf.obj (op unop) ⟶
      Y.presheaf.obj
        (op
          (Functor.obj (IsOpenEmbedding.functor sorry)
            (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop)))))
Tactic: simp only [(NatTrans.comp_app), comp_c_app, unop_op, Functor.whiskerRight_app,
      pullbackConeOfLeftFst, app_invApp_assoc, eqToHom_app, Category.assoc,
      NatTrans.naturality_assoc, restrict_carrier, comp_base, ofRestrict_base, restrict_presheaf,
      Functor.comp_obj, Functor.op_obj, Opens.map_comp_obj, TopCat.Presheaf.pushforward_obj_obj,
      Opens.carrier_eq_coe, homOfLE_leOfHom, TopCat.Presheaf.pushforward_obj_map, Functor.comp_map,
      Functor.op_map, eqToHom_unop, ofRestrict_c_app, Functor.id_obj]