-- 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
U : (Opens (↑(↑Z : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  ∀ (unop : Opens (↑(↑Z : TopCat) : Type u_1)),
    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))
⊢ Eq (α :=
    Z.presheaf.obj U ⟶
      (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
        U)
    (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))
        U :
      Z.presheaf.obj U ⟶
        (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
          U)
    (NatTrans.app (Hom.c (Y.ofRestrict ⋯ ≫ g)) U :
      Z.presheaf.obj U ⟶
        (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
          U)

Tactic:
induction U