-- 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
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : 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)
w_5 : P'.IsPrime
w_6 : 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'
obtain :
  ∀ (g : ↥(integralClosure R S)) (hgq : (↑g : S) ∉ q)
    (hg :
      Function.Bijective (α := Localization.Away g) (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
          (a : Localization.Away g) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))),
    ∃ (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 ⟨g, hgq, hg⟩ := Algebra.ZariskisMainProperty.of_finiteType (R := R) q

Premises used: Algebra.ZariskisMainProperty.of_finiteType