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

Tactic:
⟨_, _, _, inferInstance, Q, ‹_›, ‹_›, (factor₁ ..).1, (factor₂ ..).1, h₁,
    (factor₁ ..).monic, (factor₂ ..).monic, (factor₁_mul_factor₂ ..).symm,
    isCoprime_factor₁_factor₂ .., congr(($h₂).1), congr(($h₃).1)⟩

Premises used: Polynomial.MonicDegreeEq.monic, congrArg, inferInstance, Polynomial.UniversalCoprimeFactorizationRing.factor₁, id, Polynomial.UniversalCoprimeFactorizationRing.factor₂, And.intro, Exists.intro, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, Eq.symm, Subtype.val, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂