-- 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 :
  Eq.{u_2 + 1} (α := MonicDegreeEq S m × MonicDegreeEq S k)
    (↑((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]) }))
          ((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))
            q)) :
      MonicDegreeEq S m × MonicDegreeEq S k)
    (↑((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)
⊢ (↑((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]) }))
          ((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))
            q)) :
      MonicDegreeEq S m × MonicDegreeEq S k) =
    (↑q : MonicDegreeEq S m × MonicDegreeEq S k)

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