-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ ∃ (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')
have obtain : ∀ (Q : Ideal (UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))) (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 sorry (MonicDegreeEq.mk p hp sorry)))
            sorry) :
        (a : P.ResidueField) → Q.ResidueField))
  (h₂ :
    Eq (α := MonicDegreeEq Q.ResidueField f.natDegree)
      ((MonicDegreeEq.mk f hf sorry).map
        (AlgHom.toRingHom
          (Ideal.ResidueField.mapₐ P Q
            (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry)))
            sorry)))
      (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
        (factor₁ f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
        (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
          Q.ResidueField)))
  (h₃ :
    Eq (α := MonicDegreeEq Q.ResidueField g.natDegree)
      ((MonicDegreeEq.mk g hg sorry).map
        (AlgHom.toRingHom
          (Ideal.ResidueField.mapₐ P Q
            (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry)))
            sorry)))
      (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
        (factor₂ f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
        (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree sorry (MonicDegreeEq.mk p hp sorry))
          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') sorry) : (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') sorry)) f)
                  (map (algebraMap R' Q.ResidueField) f') ∧
                Eq (α := Q.ResidueField[X])
                  (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') sorry)) 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