-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens (↑Y.toTopCat : Type u)
s : (↑(Y.presheaf.obj (op U)) : Type u)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
hxU :
  Membership.mem (α := (↑(↑Y.toRingedSpace.toPresheafedSpace : TopCat) : Type u)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
hx :
  IsUnit (M :=
    (↑(Y.toRingedSpace.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y :=
            Y.toRingedSpace.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x))
            (Y.toRingedSpace.presheaf.germ U
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)
              hxU) :
          (a : (↑(Y.toRingedSpace.presheaf.obj (op U)) : Type u)) →
            (↑(Y.toRingedSpace.presheaf.stalk
                  ((ConcreteCategory.hom f.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    x)) :
              Type u))
        s :
      (↑(Y.toRingedSpace.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
⊢ x ∈
    (↑(X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
            s)) :
      Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
have h : IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := X.toRingedSpace.presheaf.obj (op ((Opens.map f.base).obj U))) (Y :=
          X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU) :
        (a : (↑(X.toRingedSpace.presheaf.obj (op ((Opens.map f.base).obj U))) : Type u)) →
          (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
            (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
              (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
          s :
        (↑((obj (Presheaf.pushforward CommRingCat f.base) X.presheaf).obj (op U)) : Type u)) :
    (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
Tactic: rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]