-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ :
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    x
h₂ : IsOpenImmersion f
f₁ :
  Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι :=
      (↑(↑(X.restrict (U :=
                Functor.obj (C := Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                  (↑(Subtype.mk (p := fun (U : Opens (↑X.toTopCat : Type u)) ↦ x ∈ U)
                        {
                          carrier :=
                            Set.range (ι :=
                              (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
                              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := TopCat.carrier) (Hom.toShHom f).hom.base) :
                                (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                                  (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
                          is_open' := ⋯ : Opens (↑X.toTopCat : Type u) }
                        h₁) :
                    Opens (↑X.toTopCat : Type u)))
                ⋯) :
            TopCat) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            (↑(X.restrict (U :=
                  Functor.obj (C := Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑(Subtype.mk (p := fun (U : Opens (↑X.toTopCat : Type u)) ↦ x ∈ U)
                          {
                            carrier :=
                              Set.range (ι :=
                                (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
                                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := TopCat.carrier) (Hom.toShHom f).hom.base) :
                                  (a :
                                      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) :
                                        Type u)) →
                                    (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
                            is_open' := ⋯ : Opens (↑X.toTopCat : Type u) }
                          h₁) :
                      Opens (↑X.toTopCat : Type u)))
                  ⋯) :
              TopCat))
            (PresheafedSpace.Hom.base (X.ofRestrict ⋯))) :
        (a : (↑(↑(X.restrict ⋯) : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
⊢ Functor.obj SheafedSpace.forgetToPresheafedSpace
      (X.restrict (U :=
          Functor.obj (C := Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
            (↑(Subtype.mk (p := fun (U : Opens (↑X.toTopCat : Type u)) ↦ x ∈ U)
                  {
                    carrier :=
                      Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) (Hom.toShHom f).hom.base) :
                          (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
                    is_open' := ⋯ : Opens (↑X.toTopCat : Type u) }
                  h₁) :
              Opens (↑X.toTopCat : Type u)))
          ⋯).toSheafedSpace ≅
    Functor.obj SheafedSpace.forgetToPresheafedSpace (Spec.toLocallyRingedSpace.obj (op R)).toSheafedSpace

Tactic:
apply PresheafedSpace.IsOpenImmersion.isoOfRangeEq (PresheafedSpace.ofRestrict _ _) f.1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq