Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : 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' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ Q,
        ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
          ∃ f' g',
            Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
              f'.Monic ∧
                g'.Monic ∧
                  map (algebraMap R R') p = f' * g' ∧
                    IsCoprime f' g' ∧
                      map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                          map (algebraMap R' Q.ResidueField) f' ∧
                        map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom 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

Goal state after:
R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : 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✝ : Q.LiesOver P
h₁ :
  Function.Bijective
    ⇑(Ideal.ResidueField.mapₐ P Q
        (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) ⋯)
h₂ :
  (MonicDegreeEq.mk f hf ⋯).map
      (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
          ⋯).toRingHom =
    (factor₁ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)).map
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField)
h₃ :
  (MonicDegreeEq.mk g hg ⋯).map
      (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
          ⋯).toRingHom =
    (factor₂ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)).map
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField)
⊢ ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ Q,
        ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
          ∃ f' g',
            Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
              f'.Monic ∧
                g'.Monic ∧
                  map (algebraMap R R') p = f' * g' ∧
                    IsCoprime f' g' ∧
                      map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                          map (algebraMap R' Q.ResidueField) f' ∧
                        map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom g =
                          map (algebraMap R' Q.ResidueField) g'