-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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
hC :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (((RingHom.comp (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap S n m k hn)) (map (algebraMap R S)))
                C :
              RingHom.{u_1, u_2} R (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
            (a : R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
          x :
        MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (((RingHom.comp
                (RingHom.comp
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift
                        (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                        (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                          (mapAlgHom (Algebra.ofId R S)))
                        ⋯ :
                      AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                        (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)))
                  (AlgHom.toRingHom (universalFactorizationMap R n m k hn)))
                C :
              RingHom.{u_1, u_2} R (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
            (a : R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
          x :
        MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
hX :
  ∀ (i : Fin n),
    Eq.{u_2 + 1} (α := MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (((RingHom.comp (AlgHom.toRingHom (universalFactorizationMap S n m k hn)) (map (algebraMap R S)) :
              RingHom.{u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
          (X i) :
        MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (((RingHom.comp
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift
                      (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                      (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                        (mapAlgHom (Algebra.ofId R S)))
                      ⋯ :
                    AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)))
                (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) :
              RingHom.{u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
          (X i) :
        MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
⊢ Eq (α := RingHom.{u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S))
    (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap S n m k hn)) (map (algebraMap R S)))
    (RingHom.comp
      (AlgHom.toRingHom
        (Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
            (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId R S)))
            ⋯ :
          AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)))
      (AlgHom.toRingHom (universalFactorizationMap R n m k hn)))

Tactic:
ext