-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    QuasiFiniteAt f x ↔
      IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) : Type u))
        {Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y))) x_1) x ⋯}
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy :
  Eq (α := ↥Y) ((Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x : ↥(Y.affineCover.X i)) : ↥Y)
    (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H :
  Eq (α := Set ↥(pullback f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
f' : (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
        (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
    Type u) →
  (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι))
    (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
      (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
    (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) ⋯
this : Topology.IsOpenEmbedding f'
h :
  IsOpen (X :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1)
            ((pullback.fst f (Y.affineCover.f i)) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1 })) ↔
    IsOpen (X := (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) : Type u))
      {f'
          (Subtype.mk (p := fun (x_1 : ↥(pullback f ι)) ↦
            Membership.mem (γ := Set ↥(pullback f ι))
              (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
                (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
              x_1)
            x ⋯)}
⊢ IsOpen (X :=
      (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
        Type u))
      (singleton (α :=
        (↑(Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y))) :
          Type u))
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1)
            ((pullback.fst f (Y.affineCover.f i)) x) ⋯ :
          { x_1 : ↥X //
            Membership.mem (γ := Set ↥X)
              (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f (Y.affineCover.f i)) x : ↥X) : ↥Y)))
              x_1 })) ↔
    IsOpen (X :=
      (↑(Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
            (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i)))) :
        Type u))
      {Subtype.mk (p := fun (x_1 : ↥(pullback f ι)) ↦
          Membership.mem (γ := Set ↥(pullback f ι))
            (Set.preimage (β := ↥(Y.affineCover.X i)) (⇑(pullback.snd f ι))
              (singleton (α := ↥(Y.affineCover.X i)) ((pullback.snd f ι) x : ↥(Y.affineCover.X i))))
            x_1)
          x ⋯}

Tactic:
rw [this.isOpen_iff_image_isOpen, Set.image_singleton]

Premises used: Set.image_singleton, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen