-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
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 : QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x
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.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 ⋯}
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) 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 }))

Tactic:
convert! this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩ using 1

Premises used: Exists.intro, rfl