-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_4 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_5 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
y : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑X.toPresheafedSpace : TopCat) : Type v))
H :
  IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            y))
        f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
H' :
  IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward C f.hom.base) X.presheaf).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
this :
  IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    ((CategoryTheory.Functor.map
          (TopCat.Presheaf.stalkFunctor C
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
              y))
          f.hom.c ≫
        TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y) ≫
      inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))
inst :
  ∀
    (this :
      IsIso (X :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            y))
        (CategoryTheory.Functor.map
            (TopCat.Presheaf.stalkFunctor C
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                y))
            f.hom.c ≫
          TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y ≫
            inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))),
    IsIso.{v, u} (X :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (Y :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (InducedCategory.Hom.hom
          (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
          this)))
inst₁ :
  ∀
    (this :
      IsIso
        (CategoryTheory.Functor.map
            (TopCat.Presheaf.stalkFunctor C
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                y))
            f.hom.c ≫
          𝟙
            (Functor.obj
              (TopCat.Presheaf.stalkFunctor C
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y))
              (Functor.obj (TopCat.Presheaf.pushforward C f.hom.base) X.presheaf)))),
    IsIso.{v, u} (X :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (Y :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (InducedCategory.Hom.hom
          (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
          this)))
inst₂ inst₃ inst₄ inst₅ :
  ∀
    (this :
      IsIso (X :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            y))
        (CategoryTheory.Functor.map
          (TopCat.Presheaf.stalkFunctor C
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
              y))
          f.hom.c)),
    IsIso.{v, u} (X :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (Y :=
      Functor.obj
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) f.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                  y)
                ⋯) :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (InducedCategory.Hom.hom
          (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
          this)))
⊢ IsIso.{v, u} (X :=
    Functor.obj
      (TopCat.Presheaf.stalkFunctor C
        (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                y)
              ⋯) :
          (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
    (Y :=
    Functor.obj
      (TopCat.Presheaf.stalkFunctor C
        (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                y)
              ⋯) :
          (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
    (CategoryTheory.Functor.map
      (TopCat.Presheaf.stalkFunctor C
        (↑(Subtype.mk (p := fun (x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) ↦ x ∈ hf.functor.obj U)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                y)
              ⋯) :
          (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (InducedCategory.Hom.hom
        (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
        this)))

Tactic:
rwa [Category.assoc, IsIso.hom_inv_id, Category.comp_id] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id