-- 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₁ :
  (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 ≅
    (Spec.toLocallyRingedSpace.obj (op R)).toSheafedSpace
⊢ 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)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)

Tactic:
apply LocallyRingedSpace.isoOfSheafedSpaceIso

Premises used: AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso