-- 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) ≫
        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))) ⋯)))) :
              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 (⋯.functor.obj (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop))))
                (eqToHom ⋯ :
                  op
                      ((Opens.map g.base).obj
                        (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj unop))) ⟶
                    op
                      (⋯.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 ⋯) (eqToHom ⋯)) :
                  op
                      (Functor.obj (IsOpenEmbedding.functor ⋯)
                        (Functor.obj (Opens.map (pullback.fst f.base g.base)) ((Opens.map f.base).obj unop))) ⟶
                    op
                      (Functor.obj (IsOpenEmbedding.functor ⋯)
                        (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) ⋯) ((Opens.map f.base).obj unop))) ⟶
                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) ⟶
      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)))))

Tactic:
rw [← Y.presheaf.map_comp, ← Y.presheaf.map_comp]

Premises used: AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp