-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
x : ↥X
hxU : x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))
obtain :
  ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i))
    (hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)),
    ∃ (V : TopologicalSpace.Opens ↥X) (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))),
      Membership.mem (α := ↥X) V ((𝒰.f i) x : ↥X) ∧
        Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
                (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                  (↑(X.presheaf.obj (Opposite.op V)) : Type u))
              ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                    (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                  s :
                (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
            (↑(X.presheaf.obj (Opposite.op V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
                (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                  (↑(X.presheaf.obj (Opposite.op V)) : Type u))
              0 :
            (↑(X.presheaf.obj (Opposite.op V)) : Type u))
⊢ ∃ (V : TopologicalSpace.Opens ↥X) (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))),
    x ∈ V ∧
      Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op V)) : Type u))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (↑(X.presheaf.obj (Opposite.op V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op V)) : Type u))
            0 :
          (↑(X.presheaf.obj (Opposite.op V)) : Type u))

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl