awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Q.IsPrime
rw : P = Ideal.comap (F := R →+* 𝓡') (algebraMap R 𝓡') Q
rw₁ : P = RingHom.ker (F := R →+* P.ResidueField) (φ.comp (algebraMap R 𝓡'))
rw₂ :
  P =
    RingHom.ker (F := R →+* P.ResidueField)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ : 𝓡' →+* P.ResidueField) (algebraMap R 𝓡'))
rw₃ : P = RingHom.ker (F := R →+* P.ResidueField) (algebraMap R P.ResidueField)
rw₄ rw₅ : P = P
⊢ P = Ideal.under R Q

Tactic:
rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]

Premises used: Ideal.ker_algebraMap_residueField, AlgHom.comp_algebraMap, RingHom.comap_ker, AlgHom.toRingHom_eq_coe, Ideal.under
-- 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
this : Q.IsPrime
⊢ Q.LiesOver P

Tactic:
have : Q.LiesOver P := ⟨by rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]⟩
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
⊢ Q.primeCompl ≤ Submonoid.comap φ (IsUnit.submonoid P.ResidueField)

Tactic:
simp [SetLike.le_def, IsUnit.mem_submonoid_iff, Q]

Premises used: SetLike.le_def, IsUnit.mem_submonoid_iff
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : Q.ResidueField
e_a : φ'.comp φi = AlgHom.id R P.ResidueField
⊢ Eq (α := P.ResidueField)
    ((φ'.comp φi : (a : P.ResidueField) → P.ResidueField) ((φ' : (a : Q.ResidueField) → P.ResidueField) x) :
      P.ResidueField)
    ((AlgHom.id R P.ResidueField : (a : P.ResidueField) → P.ResidueField)
        ((φ' : (a : Q.ResidueField) → P.ResidueField) x) :
      P.ResidueField)

Tactic:
congr
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : Q.ResidueField
⊢ φ'.comp φi = AlgHom.id R P.ResidueField

Tactic:
ext
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ φ'.comp φi = AlgHom.id R P.ResidueField

Tactic:
ext
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
x : 𝓡'
⊢ Eq (α := P.ResidueField) (((↑φ : 𝓡' →+* P.ResidueField) : (a : 𝓡') → P.ResidueField) x : P.ResidueField)
    ((e.symm : (a : Q.ResidueField) → P.ResidueField)
        ((IsScalarTower.toAlgHom R 𝓡' Q.ResidueField : (a : 𝓡') → Q.ResidueField) x) :
      P.ResidueField)

Tactic:
simp [e, φ']
-- 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
⊢ φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField

Tactic:
have H : φi.comp φ = (IsScalarTower.toAlgHom _ _ _) :=
    AlgHom.ext fun x ↦ e.eq_symm_apply.mp (by simp [e, φ'])
-- 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_1 : 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
⟨Q, ‹_›, ‹_›, e.bijective, ?_, ?_⟩

Premises used: And.intro, Exists.intro, AlgEquiv.bijective
-- 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_1 : 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine ⟨Q, ‹_›, ‹_›, e.bijective, ?_, ?_⟩
-- 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_1 : 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
trans : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
trans₁ :
  Eq (α := MonicDegreeEq Q.ResidueField m)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (φi.comp φ)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
    ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
trans ((homEquiv Q.ResidueField m k hn p) (φi.comp φ)).1.1

Premises used: Ideal.ResidueField, Prod.fst, Polynomial.UniversalCoprimeFactorizationRing.homEquiv, AlgHom.comp, Subtype.val, DFunLike.coe
-- 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_1 : 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [homEquiv_comp_fst, φ, φi]

Premises used: Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst
-- 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_1 : 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
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
rw :
  Eq (α := MonicDegreeEq Q.ResidueField m)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
    ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
⊢ Eq (α := MonicDegreeEq Q.ResidueField m)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (φi.comp φ)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
    ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))

Tactic:
rw [H]