-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
h : q'.IsPrime
hq' : q' ≠ q
h_1 : q'.LiesOver p
hxq' : x ∉ q'
simp :
  r ∉
    PrimeSpectrum.asIdeal
      ((PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ } :
          (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
            PrimeSpectrum (p.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
            x)
          { asIdeal := q', isPrime := h } ⋯))
⊢ Membership.mem (α := PrimeSpectrum (p.Fiber S)) (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S)))
    ((e :
          (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
            PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
            x)
          { asIdeal := q', isPrime := h } ⋯) :
      PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S))

Tactic:
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.preimageHomeomorphFiber,
    PrimeSpectrum.preimageOrderIsoFiber, Homeomorph.homeomorph_mk_coe, Set.mem_compl_iff,
    PrimeSpectrum.mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe, e]

Premises used: Set.singleton_subset_iff, Homeomorph.homeomorph_mk_coe, PrimeSpectrum.mem_zeroLocus, PrimeSpectrum.preimageHomeomorphFiber, SetLike.mem_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.preimageOrderIsoFiber, Set.mem_compl_iff