-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this_1 : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(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 (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
H : x ∈ s.inf W ⊓ U
this_2 : Algebra (↑R : Type u) (↑Γ(X, U) : Type u) := (CommRingCat.Hom.hom φRX).toAlgebra
this_3 : Algebra (↑R : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU))
this : Algebra (↑R : Type u) (↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
φ' : (↑A : Type u) →ₐ[(↑R : Type u)] (↑(X.presheaf.stalk x) : Type u) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : (↑Γ(X, s.inf W ⊓ U) : Type u) →ₐ[(↑R : Type u)] (↑(X.presheaf.stalk x) : Type u) :=
  let __src : (↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u) :=
    CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
i : (↑A : Type u)
hi : i ∈ (↑s : Set (↑A : Type u))
⊢ Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (↑ψ.range : Set (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) φ :
          (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        i :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
⟨X.presheaf.map (homOfLE (inf_le_left.trans (Finset.inf_le hi))).op (f i), ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, Quiver.Hom.op, setOf, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, Exists.intro, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, inf_le_left, Set.range, LE.le.trans, Finset.inf_le, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace