-- 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
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'
obtain :
  ∀ (m : ℕ) (f : R[X]) (b : p.ResidueField[X]) (hfm : f.Monic) (hbm : b.Monic)
    (hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b)
    (hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b)
    (hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)),
    ∃ (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 ⟨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'

Premises used: Ideal.ResidueField, Polynomial.X