awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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 (α := 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))
have 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])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
    (↑(↑((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])
have 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]))
Tactic: simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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 (α := 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))
have 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])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
    (↑(↑((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])
have 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]))
Tactic: simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have this : Q.IsPrime
Tactic: have : Q.IsPrime := RingHom.ker_isPrime _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ P = Ideal.under R Q
have rw : P = Ideal.comap (F := R →+* 𝓡') (algebraMap R 𝓡') Q
Tactic: rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ P = Ideal.under R Q
have rw₁ : P = RingHom.ker (F := R →+* P.ResidueField) (φ.comp (algebraMap R 𝓡'))
Tactic: rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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 𝓡'))
⊢ P = Ideal.under R Q
have rw₂ : P =
  RingHom.ker (F := R →+* P.ResidueField)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ : 𝓡' →+* P.ResidueField) (algebraMap R 𝓡'))
Tactic: rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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 𝓡'))
⊢ P = Ideal.under R Q
have rw₃ : P = RingHom.ker (F := R →+* P.ResidueField) (algebraMap R P.ResidueField)
Tactic: rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ P = Ideal.under R Q
have rw₄ : P = P
Tactic: rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have this₁ : 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]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ 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)
have e_a : φ'.comp φi = AlgHom.id R P.ResidueField
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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 φ' ⋯ ⋯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have H₁ : φ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, φ'])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
have refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine ⟨Q, ‹_›, ‹_›, e.bijective, ?_, ?_⟩