-- 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 : Opens (↑(↑Z : TopCat) : Type u_1)
refine_2 :
  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)))))
⊢ 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))

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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, AlgebraicGeometry.PresheafedSpace.comp_c_app, CategoryTheory.eqToHom_app, TopCat.Presheaf.pushforward_obj_obj, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst, TopologicalSpace.Opens.carrier_eq_coe, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.PresheafedSpace.comp_base, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, Opposite.unop_op, TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.PresheafedSpace.restrict_carrier, CategoryTheory.NatTrans.comp_app, AlgebraicGeometry.PresheafedSpace.restrict_presheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.eqToHom_unop, CategoryTheory.Functor.op_obj, AlgebraicGeometry.PresheafedSpace.ofRestrict_base, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, CategoryTheory.Functor.op_map