-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
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 : Opposite.op unop ⟶ Opposite.op unop_1
op :
  Eq (α :=
    X.presheaf.obj (Opposite.op unop) ⟶
      Y.presheaf.obj
        (Opposite.op
          (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
    (CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj unop))) (invApp f unop)
        (g.c.app (Opposite.op ((opensFunctor f).obj unop)) ≫
          Y.presheaf.map (((Opens.map g.base).map ((opensFunctor f).map i.unop)).op ≫ eqToHom ⋯)) :
      X.presheaf.obj (Opposite.op unop) ⟶
        Y.presheaf.obj
          (Opposite.op
            (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
    (CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj unop))) (invApp f unop)
        (g.c.app (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) unop)) ≫
          Y.presheaf.map
            (CategoryStruct.comp (Y :=
              Opposite.op
                (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
              (eqToHom ⋯ :
                Opposite.op ((Opens.map g.base).obj (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) unop)) ⟶
                  Opposite.op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
              (Quiver.Hom.op
                  (CategoryTheory.Functor.map (IsOpenEmbedding.functor ⋯)
                    (CategoryTheory.Functor.map (Opens.map (pullback.fst f.base g.base)) i.unop)) :
                Opposite.op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)) ⟶
                  Opposite.op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))) :
      X.presheaf.obj (Opposite.op unop) ⟶
        Y.presheaf.obj
          (Opposite.op
            (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
⊢ X.presheaf.map i ≫
      CategoryStruct.comp (Y :=
        Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop_1)))))
        (invApp f (Opposite.unop (Opposite.op unop_1)))
        (g.c.app
            (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.op unop_1)))) ≫
          Y.presheaf.map (eqToHom ⋯)) =
    CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop)))))
        (invApp f (Opposite.unop (Opposite.op unop)))
        (g.c.app
            (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.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

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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, Quiver.Hom.unop_op, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc, TopCat.Presheaf.pushforward_obj_obj, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.PresheafedSpace.restrict_carrier, CategoryTheory.Functor.map_comp, AlgebraicGeometry.PresheafedSpace.restrict_presheaf, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map