-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
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))) ⋯
⊢ 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 ⋯}
have this₁ : Topology.IsOpenEmbedding f'
Tactic: have : Topology.IsOpenEmbedding f' := by
      convert!
        (f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding using 0
      dsimp [f', Set.restrictPreimage]
      congr!