-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
obtain :
  ∀ (Q : Ideal (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) (w : Q.IsPrime)
    (w_1 : Q.LiesOver P)
    (h₁ :
      Function.Bijective (α := P.ResidueField) (β := Q.ResidueField)
        (⇑(Ideal.ResidueField.mapₐ P Q
              (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
              ⋯) :
          (a : P.ResidueField) → Q.ResidueField))
    (h₂ :
      Eq (α := MonicDegreeEq Q.ResidueField f.natDegree)
        ((MonicDegreeEq.mk f hf ⋯).map
          (AlgHom.toRingHom
            (Ideal.ResidueField.mapₐ P Q
              (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
              ⋯)))
        (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
          (factor₁ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
          (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
            Q.ResidueField)))
    (h₃ :
      Eq (α := MonicDegreeEq Q.ResidueField g.natDegree)
        ((MonicDegreeEq.mk g hg ⋯).map
          (AlgHom.toRingHom
            (Ideal.ResidueField.mapₐ P Q
              (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
              ⋯)))
        (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
          (factor₂ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
          (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
            Q.ResidueField))),
    ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Algebra.Etale R R') (Q : Ideal R') (x_3 : Q.IsPrime)
      (x_4 : Q.LiesOver P) (f' : R'[X]) (g' : R'[X]),
      Function.Bijective (α := P.ResidueField) (β := Q.ResidueField)
          (⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) : (a : P.ResidueField) → Q.ResidueField) ∧
        f'.Monic ∧
          g'.Monic ∧
            map (algebraMap R R') p = f' * g' ∧
              IsCoprime f' g' ∧
                Eq (α := Q.ResidueField[X])
                    (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) f)
                    (map (algebraMap R' Q.ResidueField) f') ∧
                  Eq (α := Q.ResidueField[X])
                    (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) g)
                    (map (algebraMap R' Q.ResidueField) g')
⊢ ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Algebra.Etale R R') (Q : Ideal R') (x_3 : Q.IsPrime) (x_4
    : Q.LiesOver P) (f' : R'[X]) (g' : R'[X]),
    Function.Bijective (α := P.ResidueField) (β := Q.ResidueField)
        (⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) : (a : P.ResidueField) → Q.ResidueField) ∧
      f'.Monic ∧
        g'.Monic ∧
          map (algebraMap R R') p = f' * g' ∧
            IsCoprime f' g' ∧
              Eq (α := Q.ResidueField[X]) (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) f)
                  (map (algebraMap R' Q.ResidueField) f') ∧
                Eq (α := Q.ResidueField[X])
                  (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) g)
                  (map (algebraMap R' Q.ResidueField) g')

Tactic:
obtain ⟨Q, _, _, h₁, h₂, h₃⟩ :=
    exists_liesOver_residueFieldMap_bijective f.natDegree g.natDegree
    (by simpa [hf.natDegree_mul hg, hp.natDegree_map] using congr(($H).natDegree)) (.mk p hp rfl)
    P (.mk f hf rfl) (.mk g hg rfl) H Hpq

Premises used: Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, Polynomial.MonicDegreeEq.mk, Polynomial.natDegree, rfl