Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ e,
            ∃ (_ : IsIdempotentElem e),
              ∃ e₀,
                ∃ (_ : IsIdempotentElem e₀) (_ :
                  (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e),
                  ∃ P',
                    ∃ (_ : P'.IsPrime) (_ : P'.LiesOver P),
                      Ideal.comap TensorProduct.includeRight.toRingHom P' = q ∧
                        e ∉ P' ∧
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                            (∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
                                P''.IsPrime →
                                  P''.LiesOver P →
                                    e₀ ∉ P'' →
                                      P'' =
                                        Ideal.comap
                                          (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom
                                          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

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
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 → ⟨s, hRs⟩ ∈ q'
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ e,
            ∃ (_ : IsIdempotentElem e),
              ∃ e₀,
                ∃ (_ : IsIdempotentElem e₀) (_ :
                  (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e),
                  ∃ P',
                    ∃ (_ : P'.IsPrime) (_ : P'.LiesOver P),
                      Ideal.comap TensorProduct.includeRight.toRingHom P' = q ∧
                        e ∉ P' ∧
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                            (∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
                                P''.IsPrime →
                                  P''.LiesOver P →
                                    e₀ ∉ P'' →
                                      P'' =
                                        Ideal.comap
                                          (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom
                                          P') ∧
                              ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'