-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
this :
  ∀ {X : Scheme.{u}} {x : ↥X} (R : CommRingCat.{u}) {f : X ⟶ Spec R} [LocallyOfFiniteType f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f x : ↥(Spec R)))) x_1)
            x ⋯}
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1)
            ((X.affineCover.f i) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
              x_1 })) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) : Type u))
      {Subtype.mk (p := fun (x_1 : ↥(X.affineCover.X i)) ↦
          Membership.mem (γ := Set ↥(X.affineCover.X i))
            (Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) x_1)
          x ⋯}
have h : IsOpen (X :=
    (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
      Type u))
    (singleton (α :=
      (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R)))) :
        Type u))
      (Subtype.mk (p := fun (x_1 : ↥X) ↦
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
            x_1)
          ((X.affineCover.f i) x) sorry :
        { x_1 : ↥X //
          Membership.mem (γ := Set ↥X)
            (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f ((X.affineCover.f i) x) : ↥(Spec R))))
            x_1 })) ↔
  IsOpen (X := (↑(Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f (ι x) : ↥(Spec R)))) : Type u))
    {Set.restrictPreimage (Set.preimage (β := ↥(Spec R)) (⇑f) (singleton (α := ↥(Spec R)) (f (ι x) : ↥(Spec R)))) (⇑ι)
        (Subtype.mk (p := fun (x_1 : ↥(X.affineCover.X i)) ↦
          Membership.mem (γ := Set ↥(X.affineCover.X i))
            (Set.preimage (β := ↥(Spec R)) (⇑(ι ≫ f)) (singleton (α := ↥(Spec R)) ((ι ≫ f) x : ↥(Spec R)))) x_1)
          x sorry)}
Tactic: rw [((f ⁻¹' {f (ι x)}).restrictPreimage_isOpenEmbedding
      ι.isOpenEmbedding).isOpen_iff_image_isOpen, Set.image_singleton]