-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
this :
  ∀ {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))) ⋯
⊢ Topology.IsOpenEmbedding f' ↔
    Topology.IsOpenEmbedding (X :=
      (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
            (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
        Type u))
      (Set.restrictPreimage (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))
        ⇑(pullback.fst f ι))
have a : Topology.IsOpenEmbedding (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))
    (Y := (↑(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))) sorry) ↔
  Topology.IsOpenEmbedding (X :=
    (↑(Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
          (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y)))) :
      Type u))
    (Set.MapsTo.restrict (⇑(pullback.fst f ι))
      (Set.preimage (β := ↥X) (⇑(pullback.fst f ι))
        (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))))
      (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f ((pullback.fst f ι) x : ↥X) : ↥Y))) sorry)
Tactic: dsimp [f', Set.restrictPreimage]