-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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
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) ⋯ :
          { 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 ⋯)}
⊢ 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 ⋯}

Tactic:
rw [((f ⁻¹' {f (ι x)}).restrictPreimage_isOpenEmbedding
      ι.isOpenEmbedding).isOpen_iff_image_isOpen, Set.image_singleton]

Premises used: Set.image_singleton, Set.restrictPreimage_isOpenEmbedding, CategoryTheory.ConcreteCategory.hom, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Set.preimage, AlgebraicGeometry.PresheafedSpace.Hom.base, Singleton.singleton, DFunLike.coe