-- 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 unop_1 : Opens (↑(↑X : TopCat) : Type u_1)
i : op unop ⟶ op unop_1
⊢ X.presheaf.map i ≫
      CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj (Opposite.unop (op unop_1)))))
        (invApp f (Opposite.unop (op unop_1)))
        (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (op unop_1)))) ≫
          Y.presheaf.map (eqToHom ⋯)) =
    CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj (Opposite.unop (op unop)))))
        (invApp f (Opposite.unop (op unop)))
        (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (op unop)))) ≫
          Y.presheaf.map (eqToHom ⋯)) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (pullback.fst f.base g.base))
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).map
        i
have op : Eq (α :=
  X.presheaf.obj (op unop) ⟶
    Y.presheaf.obj
      (op (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
  (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj unop))) (invApp f unop)
      (g.c.app (op ((opensFunctor f).obj unop)) ≫
        Y.presheaf.map (((Opens.map g.base).map ((opensFunctor f).map i.unop)).op ≫ eqToHom sorry)) :
    X.presheaf.obj (op unop) ⟶
      Y.presheaf.obj
        (op (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
  (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj unop))) (invApp f unop)
      (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) unop)) ≫
        Y.presheaf.map
          (CategoryStruct.comp (Y :=
            op (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
            (eqToHom sorry :
              op ((Opens.map g.base).obj (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) unop)) ⟶
                op
                  (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
            (Quiver.Hom.op
                (CategoryTheory.Functor.map (IsOpenEmbedding.functor sorry)
                  (CategoryTheory.Functor.map (Opens.map (pullback.fst f.base g.base)) i.unop)) :
              op (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)) ⟶
                op
                  (Functor.obj (IsOpenEmbedding.functor sorry)
                    (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))) :
    X.presheaf.obj (op unop) ⟶
      Y.presheaf.obj
        (op (Functor.obj (IsOpenEmbedding.functor sorry) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
Tactic: simp only [(inv_naturality_assoc), restrict_carrier, restrict_presheaf,
          TopCat.Presheaf.pushforward_obj_obj, Functor.comp_obj, Functor.op_obj,
          TopCat.Presheaf.pushforward_obj_map, Functor.comp_map, Functor.op_map, Quiver.Hom.unop_op,
          NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op,
          ← Functor.map_comp, Category.assoc]