-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑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)) → (↑(↑Y : TopCat) : Type u_1))
simp :
  Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U))))
    (Y.presheaf.map
      (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)) → (↑(↑Y : 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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            (↑U : Set (↑(↑Y : TopCat) : Type u_1))))
        (Y := (↑U : Set (↑(↑Y : 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)) → (↑(↑Y : 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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
              (↑U : Set (↑(↑Y : TopCat) : Type u_1))))
          (y := (↑U : Set (↑(↑Y : TopCat) : Type u_1))) ⋯)))
    (Y.presheaf.map (eqToHom ⋯))
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U))))
    (f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U))
    (Y.presheaf.map
      (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)) → (↑(↑Y : 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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            U.carrier))
        (Y := U.carrier)
        (eqToHom (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)) → (↑(↑Y : 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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
              U.carrier))
          (Y := U.carrier) ⋯)))

Tactic:
simp only [TopCat.Presheaf.pushforward_obj_obj, app_invApp, Opens.carrier_eq_coe,
    homOfLE_leOfHom, eqToHom_op]

Premises used: TopCat.Presheaf.pushforward_obj_obj, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, TopologicalSpace.Opens.carrier_eq_coe, CategoryTheory.eqToHom_op