-- 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 :
  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 := inst_4 } ⋯))
rw :
  ∀
    (this :
      1 ⊗ₜ[R] x ∉
        RingHom.ker (F :=
          { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] 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 : PrimeSpectrum S } ⋯ :
                      { x : PrimeSpectrum S //
                        Membership.mem (γ := Set (PrimeSpectrum S))
                          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                          x }) :
                  PrimeSpectrum S).asIdeal.ResidueField)
          (AlgHom.toRingHom
            (TensorProduct.lift
                (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := ⋯ }.asIdeal
                  (↑(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 } ⋯ :
                          { x : PrimeSpectrum S //
                            Membership.mem (γ := Set (PrimeSpectrum S))
                              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                              x }) :
                      PrimeSpectrum S).asIdeal
                  (ofId R S) ⋯)
                (IsScalarTower.toAlgHom R 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 : PrimeSpectrum S } ⋯ :
                            { x : PrimeSpectrum S //
                              Membership.mem (γ := Set (PrimeSpectrum S))
                                (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                  {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                                x }) :
                        PrimeSpectrum S).asIdeal.ResidueField)
                ⋯ :
              { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →ₐ[R]
                (↑(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 : PrimeSpectrum S } ⋯ :
                          { x : PrimeSpectrum S //
                            Membership.mem (γ := Set (PrimeSpectrum S))
                              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                              x }) :
                      PrimeSpectrum S).asIdeal.ResidueField))),
    x ∉ q
rw₁ :
  ∀
    (this :
      r ∉
        RingHom.ker (F :=
          { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] 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 : PrimeSpectrum S } ⋯ :
                      { x : PrimeSpectrum S //
                        Membership.mem (γ := Set (PrimeSpectrum S))
                          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                            {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                          x }) :
                  PrimeSpectrum S).asIdeal.ResidueField)
          (AlgHom.toRingHom
            (TensorProduct.lift
                (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := ⋯ }.asIdeal
                  (↑(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 } ⋯ :
                          { x : PrimeSpectrum S //
                            Membership.mem (γ := Set (PrimeSpectrum S))
                              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                              x }) :
                      PrimeSpectrum S).asIdeal
                  (ofId R S) ⋯)
                (IsScalarTower.toAlgHom R 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 : PrimeSpectrum S } ⋯ :
                            { x : PrimeSpectrum S //
                              Membership.mem (γ := Set (PrimeSpectrum S))
                                (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                  {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                                x }) :
                        PrimeSpectrum S).asIdeal.ResidueField)
                ⋯ :
              { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →ₐ[R]
                (↑(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 : PrimeSpectrum S } ⋯ :
                          { x : PrimeSpectrum S //
                            Membership.mem (γ := Set (PrimeSpectrum S))
                              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                              x }) :
                      PrimeSpectrum S).asIdeal.ResidueField))),
    ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) s : p.Fiber S) ∉
      RingHom.ker (F :=
        { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] 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 : PrimeSpectrum S } ⋯ :
                    { x : PrimeSpectrum S //
                      Membership.mem (γ := Set (PrimeSpectrum S))
                        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                        x }) :
                PrimeSpectrum S).asIdeal.ResidueField)
        (AlgHom.toRingHom
          (TensorProduct.lift
              (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := ⋯ }.asIdeal
                (↑(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 } ⋯ :
                        { x : PrimeSpectrum S //
                          Membership.mem (γ := Set (PrimeSpectrum S))
                            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                            x }) :
                    PrimeSpectrum S).asIdeal
                (ofId R S) ⋯)
              (IsScalarTower.toAlgHom R 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 : PrimeSpectrum S } ⋯ :
                          { x : PrimeSpectrum S //
                            Membership.mem (γ := Set (PrimeSpectrum S))
                              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                                {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                              x }) :
                      PrimeSpectrum S).asIdeal.ResidueField)
              ⋯ :
            { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →ₐ[R]
              (↑(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 : PrimeSpectrum S } ⋯ :
                        { x : PrimeSpectrum S //
                          Membership.mem (γ := Set (PrimeSpectrum S))
                            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
                            x }) :
                    PrimeSpectrum S).asIdeal.ResidueField))
⊢ x ∉ q

Tactic:
rw [PrimeSpectrum.preimageEquivFiber_apply_asIdeal,
        ← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ s), ← Algebra.smul_def, hsx] at this

Premises used: PrimeSpectrum.preimageEquivFiber_apply_asIdeal, Algebra.smul_def, Ideal.IsPrime.mul_mem_left_iff