-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
this_1 : IsIso (X := pullback f g) (pullback.snd f g)
this :
  Eq (α := (↑(pullback f g).toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g))
      (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)))
    (PresheafedSpace.Hom.base (Hom.toHom (pullback.fst f g)))
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h :
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      {x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1) |
        ∃ (y : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)),
          Eq (α := (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
                x :
              (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) :
                  (a : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)) →
                    (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
                y :
              (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))}
      x →
    Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
        (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
      x
⊢ Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      {x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1) |
        ∃ (y : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)),
          Eq (α := (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
                x :
              (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) :
                  (a : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)) →
                    (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
                y :
              (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))}
      x ↔
    Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
        (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
      x
have h₁ : Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
      (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
    x →
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    {x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1) |
      ∃ (y : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)),
        Eq (α := (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
              x :
            (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) :
                (a : (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y) : Type u_1)) →
                  (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))
              y :
            (↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Z) : Type u_1))}
    x
Tactic: constructor