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
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'

Tactic:
obtain ⟨m, f, b, hfm, hbm, hab, hfab, hf⟩ : ∃ (m : ℕ) (f : R[X])
      (b : p.ResidueField[X]), f.Monic ∧ b.Monic ∧ IsCoprime (X ^ (m + 1)) b ∧
        f.map (algebraMap _ _) = X ^ (m + 1) * b ∧ aeval s f = 0 := by
    let f := X * minpoly R s
    obtain ⟨q, hq, hq'⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd
      ((minpoly R s).map (algebraMap R p.ResidueField)) ((minpoly.monic hRs).map _).ne_zero 0
    have hqm : q.Monic := by
      simpa [((minpoly.monic hRs).map _).leadingCoeff] using! congr(leadingCoeff $hq).symm
    set m' := rootMultiplicity 0 ((minpoly R s).map (algebraMap R p.ResidueField))
    refine ⟨m', f, q, monic_X.mul (minpoly.monic hRs), hqm, ?_,
      by simp [f, hq, pow_succ', mul_assoc], by simp [f]⟩
    simpa [IsCoprime.pow_left_iff,
      (prime_X (R := p.ResidueField)).irreducible.coprime_iff_not_dvd] using! hq'

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'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
⊢ ∃ 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'