-- 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
H :
  ∀ (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)
⊢ 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) ⋯))
              ⋯ :
            𝓡' →ₐ[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 𝓡 𝓡'))
    (f.comp (Algebra.algHom R 𝓡 𝓡'))

Tactic:
ext