-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ (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) =
    f
have apply : Eq (α := 𝓡 →ₐ[R] 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) sorry))
            sorry :
          𝓡' →ₐ[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)
              sorry :
            { 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 𝓡 𝓡'))
  (f.comp (Algebra.algHom R 𝓡 𝓡'))
Tactic: apply IsLocalization.algHom_ext
      (.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)