awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[R] S)
    (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
rw :
  IsCoprime (R := S[X]) (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
    (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
⊢ IsUnit
    (resultant (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
      (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).natDegree
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]).natDegree)

Tactic:
rw [← (UniversalFactorizationRing.factor₁ m k hn p).monic.natDegree_map f.toRingHom,
      ← (UniversalFactorizationRing.factor₂ m k hn p).monic.natDegree_map f.toRingHom,
      AlgHom.toRingHom_eq_coe, Polynomial.isUnit_resultant_iff_isCoprime
        ((UniversalFactorizationRing.factor₁ m k hn p).monic.map _)]

Premises used: Polynomial.MonicDegreeEq.monic, Polynomial.UniversalFactorizationRing.factor₂, Polynomial.UniversalFactorizationRing.factor₁, Polynomial.isUnit_resultant_iff_isCoprime, Polynomial.Monic.natDegree_map, AlgHom.toRingHom, AlgHom.toRingHom_eq_coe, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[R] S)
    (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
⊢ IsCoprime.{u_2} (R := S[X])
    (↑(↑((UniversalFactorizationRing.homEquiv S m k hn p :
                  (a : 𝓡 →ₐ[R] S) →
                    { q : MonicDegreeEq S m × MonicDegreeEq S k //
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
                f) :
            MonicDegreeEq S m × MonicDegreeEq S k).1 :
      S[X])
    (↑(↑((UniversalFactorizationRing.homEquiv S m k hn p :
                  (a : 𝓡 →ₐ[R] S) →
                    { q : MonicDegreeEq S m × MonicDegreeEq S k //
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
                f) :
            MonicDegreeEq S m × MonicDegreeEq S k).2 :
      S[X])

Tactic:
simpa [f] using q.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : 𝓡' →ₐ[R] S
x : 𝓡
⊢ Eq.{u_2 + 1} (α := S)
    ((AlgHom.comp (B := 𝓡')
            ((fun
                  (q :
                    { q : MonicDegreeEq S m × MonicDegreeEq S k //
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }) ↦
                (IsLocalization.liftAlgHom (R := 𝓡) (M :=
                    Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
                    (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
                        (a :
                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                          𝓡 →ₐ[R] S)
                      (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                        (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯))
                    ⋯ :
                  𝓡' →ₐ[R] S))
              ((fun (f : 𝓡' →ₐ[R] S) ↦
                  (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]))
                      (↑((UniversalFactorizationRing.homEquiv S m k hn p :
                              (a : 𝓡 →ₐ[R] S) →
                                { q : MonicDegreeEq S m × MonicDegreeEq S k //
                                  (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
                            (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))) :
                        MonicDegreeEq S m × MonicDegreeEq S k)
                      ⋯ :
                    { q : MonicDegreeEq S m × MonicDegreeEq S k //
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }))
                f))
            (Algebra.algHom R 𝓡 𝓡') :
          (a : 𝓡) → S)
        x :
      S)
    ((f.comp (Algebra.algHom R 𝓡 𝓡') : (a : 𝓡) → S) x : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
⊢ (↑((UniversalFactorizationRing.homEquiv S m k hn p :
            (a : 𝓡 →ₐ[R] S) →
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
          ((Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
              (a :
                  { q : MonicDegreeEq S m × MonicDegreeEq S k //
                    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                𝓡 →ₐ[R] S)
            (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
              (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯))) :
      MonicDegreeEq S m × MonicDegreeEq S k) =
    (↑(Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k)
          ⋯) :
      MonicDegreeEq S m × MonicDegreeEq S k)

Tactic:
congr($((UniversalFactorizationRing.homEquiv S m k hn p).apply_symm_apply
      ⟨_, q.2.1⟩).1)

Premises used: Equiv.apply_symm_apply, congrArg, Polynomial.UniversalFactorizationRing.homEquiv, id, Subtype.mk, And.left, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
h :
  ∀ (x : 𝓡),
    Eq.{u_2 + 1} (α := S)
      ((AlgHom.comp (B := 𝓡')
              (IsLocalization.liftAlgHom (R := 𝓡) (M :=
                Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
                (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
                    (a :
                        { q : MonicDegreeEq S m × MonicDegreeEq S k //
                          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                      𝓡 →ₐ[R] S)
                  (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                    (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯))
                ⋯)
              (IsScalarTower.toAlgHom R 𝓡 𝓡') :
            (a : 𝓡) → S)
          x :
        S)
      ((((Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
                  (a :
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                    𝓡 →ₐ[R] S)
                (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                  (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯) :
              𝓡 →ₐ[R] S) :
            (a : 𝓡) → S)
          x :
        S)
⊢ Eq (α := 𝓡 →ₐ[R] S)
    (AlgHom.comp (B := 𝓡')
      (IsLocalization.liftAlgHom (R := 𝓡) (M :=
        Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
        (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
            (a :
                { q : MonicDegreeEq S m × MonicDegreeEq S k //
                  (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
              𝓡 →ₐ[R] S)
          (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
            (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯))
        ⋯)
      (IsScalarTower.toAlgHom R 𝓡 𝓡'))
    ((Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
        (a :
            { q : MonicDegreeEq S m × MonicDegreeEq S k //
              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
          𝓡 →ₐ[R] S)
      (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k)
        ⋯))

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
x : 𝓡
⊢ Eq.{u_2 + 1} (α := S)
    ((AlgHom.comp (B := 𝓡')
            (IsLocalization.liftAlgHom (R := 𝓡) (M :=
              Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
              (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
                  (a :
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                    𝓡 →ₐ[R] S)
                (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                  (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯))
              ⋯)
            (IsScalarTower.toAlgHom R 𝓡 𝓡') :
          (a : 𝓡) → S)
        x :
      S)
    ((((Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
                (a :
                    { q : MonicDegreeEq S m × MonicDegreeEq S k //
                      (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
                  𝓡 →ₐ[R] S)
              (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯) :
            𝓡 →ₐ[R] S) :
          (a : 𝓡) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
a :
  Eq (α := T[X])
    (↑(↑((homEquiv T m k hn p :
                  (a : 𝓡' →ₐ[R] T) →
                    { q : MonicDegreeEq T m × MonicDegreeEq T k //
                      (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
                (g.comp f)) :
            MonicDegreeEq T m × MonicDegreeEq T k).1 :
      T[X])
    (↑(MonicDegreeEq.map
          (↑((homEquiv S m k hn p :
                    (a : 𝓡' →ₐ[R] S) →
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                          IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
                  f) :
              MonicDegreeEq S m × MonicDegreeEq S k).1
          (↑g : S →+* T)) :
      T[X])
⊢ Eq (α := MonicDegreeEq T m)
    (↑((homEquiv T m k hn p :
              (a : 𝓡' →ₐ[R] T) →
                { q : MonicDegreeEq T m × MonicDegreeEq T k //
                  (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
            (g.comp f)) :
        MonicDegreeEq T m × MonicDegreeEq T k).1
    (MonicDegreeEq.map
      (↑((homEquiv S m k hn p :
                (a : 𝓡' →ₐ[R] S) →
                  { q : MonicDegreeEq S m × MonicDegreeEq S k //
                    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                      IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
              f) :
          MonicDegreeEq S m × MonicDegreeEq S k).1
      (↑g : S →+* T))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
a :
  Eq (α := T[X])
    (map (↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* T)
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
    (map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T)
        (↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* S))
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
⊢ Eq (α := T[X])
    (↑(↑((homEquiv T m k hn p :
                  (a : 𝓡' →ₐ[R] T) →
                    { q : MonicDegreeEq T m × MonicDegreeEq T k //
                      (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
                (g.comp f)) :
            MonicDegreeEq T m × MonicDegreeEq T k).1 :
      T[X])
    (↑(MonicDegreeEq.map
          (↑((homEquiv S m k hn p :
                    (a : 𝓡' →ₐ[R] S) →
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                          IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
                  f) :
              MonicDegreeEq S m × MonicDegreeEq S k).1
          (↑g : S →+* T)) :
      T[X])

Tactic:
simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]

Premises used: Polynomial.UniversalFactorizationRing.homEquiv, Polynomial.UniversalCoprimeFactorizationRing.homEquiv, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ Eq (α := T[X])
    (map (↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* T)
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
    (map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T)
        (↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* S))
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
a :
  Eq (α := T[X])
    (↑(↑((homEquiv T m k hn p :
                  (a : 𝓡' →ₐ[R] T) →
                    { q : MonicDegreeEq T m × MonicDegreeEq T k //
                      (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
                (g.comp f)) :
            MonicDegreeEq T m × MonicDegreeEq T k).2 :
      T[X])
    (↑(MonicDegreeEq.map
          (↑((homEquiv S m k hn p :
                    (a : 𝓡' →ₐ[R] S) →
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                          IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
                  f) :
              MonicDegreeEq S m × MonicDegreeEq S k).2
          (↑g : S →+* T)) :
      T[X])
⊢ Eq (α := MonicDegreeEq T k)
    (↑((homEquiv T m k hn p :
              (a : 𝓡' →ₐ[R] T) →
                { q : MonicDegreeEq T m × MonicDegreeEq T k //
                  (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
            (g.comp f)) :
        MonicDegreeEq T m × MonicDegreeEq T k).2
    (MonicDegreeEq.map
      (↑((homEquiv S m k hn p :
                (a : 𝓡' →ₐ[R] S) →
                  { q : MonicDegreeEq S m × MonicDegreeEq S k //
                    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                      IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
              f) :
          MonicDegreeEq S m × MonicDegreeEq S k).2
      (↑g : S →+* T))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
a :
  Eq (α := T[X])
    (map (↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* T)
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
    (map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T)
        (↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* S))
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
⊢ Eq (α := T[X])
    (↑(↑((homEquiv T m k hn p :
                  (a : 𝓡' →ₐ[R] T) →
                    { q : MonicDegreeEq T m × MonicDegreeEq T k //
                      (↑q.1 : T[X]) * (↑q.2 : T[X]) = map (algebraMap R T) (↑p : R[X]) ∧
                        IsCoprime (↑q.1 : T[X]) (↑q.2 : T[X]) })
                (g.comp f)) :
            MonicDegreeEq T m × MonicDegreeEq T k).2 :
      T[X])
    (↑(MonicDegreeEq.map
          (↑((homEquiv S m k hn p :
                    (a : 𝓡' →ₐ[R] S) →
                      { q : MonicDegreeEq S m × MonicDegreeEq S k //
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧
                          IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) })
                  f) :
              MonicDegreeEq S m × MonicDegreeEq S k).2
          (↑g : S →+* T)) :
      T[X])

Tactic:
simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]

Premises used: Polynomial.UniversalFactorizationRing.homEquiv, Polynomial.UniversalCoprimeFactorizationRing.homEquiv, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst_3 : CommRing T
inst_4 : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ Eq (α := T[X])
    (map (↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* T)
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
    (map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* T)
        (↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) : 𝓡 →+* S))
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
⊢ Q.IsPrime

Tactic:
have : Q.IsPrime := RingHom.ker_isPrime _