-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
obtain :
  ∀ (s : S) (hsq : s ∉ q) (hRs : IsIntegral R s) (hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q')
    (hs₀ :
      ∀ (q' : Ideal ↥(integralClosure R S)),
        q'.IsPrime →
          q' ≠ Ideal.under (↥(integralClosure R S)) q →
            q'.LiesOver p →
              Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'),
    ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (P : Ideal R') (x_3 : P.IsPrime) (x_4 :
      P.LiesOver p) (e : R' ⊗[R] S) (_ : IsIdempotentElem e) (e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
      (_ : IsIdempotentElem e₀) (_ :
      ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
              TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
            (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
          e₀ =
        e)
      (P' : Ideal (R' ⊗[R] S)) (_ : P'.IsPrime) (_ : P'.LiesOver P),
      Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q ∧
        e ∉ P' ∧
          Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
              (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField) ∧
            (∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
                P''.IsPrime →
                  P''.LiesOver P →
                    e₀ ∉ P'' →
                      P'' =
                        Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
                          (AlgHom.toRingHom
                            (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                              TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
                          P') ∧
              ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
⊢ ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (P : Ideal R') (x_3 : P.IsPrime) (x_4 :
    P.LiesOver p) (e : R' ⊗[R] S) (_ : IsIdempotentElem e) (e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)) (_
    : IsIdempotentElem e₀) (_ :
    ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
            TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
          (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
        e₀ =
      e)
    (P' : Ideal (R' ⊗[R] S)) (_ : P'.IsPrime) (_ : P'.LiesOver P),
    Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q ∧
      e ∉ P' ∧
        Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
            (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField) ∧
          (∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
              P''.IsPrime →
                P''.LiesOver P →
                  e₀ ∉ P'' →
                    P'' =
                      Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
                        (AlgHom.toRingHom
                          (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                            TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
                        P') ∧
            ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'

Tactic:
obtain ⟨s, hsq, hRs, hs, hs₀⟩ := exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver p q

Premises used: Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver