-- 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'
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)
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) (a' b' : R'[X])
        (hP :
          Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
            (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField))
        (ha'm : a'.Monic) (hb'm : b'.Monic) (hfab' : Polynomial.map (algebraMap R R') f = a' * b') (c d : R'[X])
        (hcd : c * a' + d * b' = 1)
        (ha' :
          Eq (α := P.ResidueField[X])
            (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
              (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
            (Polynomial.map (algebraMap R' P.ResidueField) a'))
        (hb' :
          Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
            (Polynomial.map (algebraMap R' P.ResidueField) b')),
        ∃ (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 ⟨R', _, _, _, P, _, _, a', b', hP, ha'm, hb'm, hfab', ⟨c, d, hcd⟩, ha', hb'⟩ :=
    Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime p f
      (X ^ (m + 1)) b hfm (monic_X.pow _) hbm hfab hab

Premises used: HPow.hPow, HAdd.hAdd, Polynomial.Monic.pow, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, OfNat.ofNat, Polynomial.X, Polynomial.monic_X