-- 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 :
  ∀ (R' : Type u) (w : CommRing R') (w_1 : Algebra R R'),
    Etale R R' →
      ∀ (P : Ideal R') (w_3 : P.IsPrime) (w_4 : P.LiesOver p) (e : R' ⊗[R] S) (he : IsIdempotentElem e)
        (e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)) (he₀ : IsIdempotentElem e₀)
        (he₀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 →
            ∀ (hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q)
              (heP' : e ∉ P')
              (hpP :
                Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
                  (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField))
              (H' :
                ∀ (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')
              (H : ∀ (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) (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) ∧
                      Module.Finite R' (Localization.Away e) ∧
                        ∀ (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) (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) ∧
          Module.Finite R' (Localization.Away e) ∧
            ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'

Tactic:
obtain ⟨R', _, _, _, P, _, _, e, he, e₀, he₀, he₀e, P', _, _, hP'q, heP', hpP, H', H⟩ :=
    exists_etale_isIdempotentElem_forall_liesOver_eq_aux p q

Premises used: Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux