-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
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 : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ ((Opens.map f.base).obj U) x hxU) :
          (a : (↑(X.presheaf.obj (op ((Opens.map f.base).obj U))) : Type u)) → (↑(X.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.presheaf.stalk x) : Type u))
h :
  IsUnit (M :=
    (↑(Y.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.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.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.presheaf.obj (op U)) : Type u)) →
            (↑(Y.presheaf.stalk
                  ((ConcreteCategory.hom f.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    x)) :
              Type u))
        s :
      (↑(Y.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))
⊢ Membership.mem (α := (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) (RingedSpace.basicOpen Y.toSheafedSpace s)
    ((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))

Tactic:
rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.RingedSpace.mem_basicOpen