-- 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) ⟶
      Y.presheaf.obj
        (op
          (Functor.obj (IsOpenEmbedding.functor ⋯)
            (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))) ⋯))))) :
            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 ⋯)
                    (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop)))))
              (Y.presheaf.map (eqToHom ⋯) :
                Y.presheaf.obj
                    (op
                      ((Opens.map g.base).obj
                        (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj unop)))) ⟶
                  Y.presheaf.obj
                    (op
                      (⋯.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 ⋯) (eqToHom ⋯))) :
                Y.presheaf.obj
                    (op
                      (Functor.obj (IsOpenEmbedding.functor ⋯)
                        (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop)))) ⟶
                  Y.presheaf.obj
                    (op
                      (Functor.obj (IsOpenEmbedding.functor ⋯)
                        (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 ⋯)
                    (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 ⋯)
              (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 ⋯)) ((Opens.map g.base).obj unop))) :
      Z.presheaf.obj (op unop) ⟶
        Y.presheaf.obj
          (op
            (Functor.obj (IsOpenEmbedding.functor ⋯)
              (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj 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) ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map g.base).obj ((opensFunctor f).obj ((Opens.map f.base).obj unop))))
          (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)))) :
            op ((Opens.map g.base).obj unop) ⟶
              op ((Opens.map g.base).obj ((opensFunctor f).obj ((Opens.map f.base).obj unop))))
          (CategoryStruct.comp (Y :=
              op (sorry.functor.obj (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop))))
              (eqToHom sorry :
                op
                    ((Opens.map g.base).obj
                      (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) ((Opens.map f.base).obj unop))) ⟶
                  op
                    (sorry.functor.obj
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop))))
              (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor sorry) (eqToHom sorry)) :
                op
                    (Functor.obj (IsOpenEmbedding.functor sorry)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop))) ⟶
                  op
                    (Functor.obj (IsOpenEmbedding.functor sorry)
                      (Functor.obj (Opens.map (pullback.snd f.base g.base)) ((Opens.map g.base).obj unop)))) :
            op
                ((Opens.map g.base).obj
                  (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) ((Opens.map f.base).obj unop))) ⟶
              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: rw [← Y.presheaf.map_comp, ← Y.presheaf.map_comp]