-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x, hxU