-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
h : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
inr :
  ∀ (x : R),
    Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(aeval
                      (Algebra.Generators.val
                        (Algebra.Presentation.toGenerators
                          (Algebra.PreSubmersivePresentation.toPresentation
                            (universalFactorizationMapPresentation R n m k hn))))) :
                  MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+*
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)) :
                  MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
              C :
            (a : R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          x :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((RingHom.comp
              (↑Algebra.TensorProduct.includeRight :
                MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              C :
            (a : R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          x :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
inr₁ :
  ∀ (i : Fin k),
    Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(aeval
                    (Algebra.Generators.val
                      (Algebra.Presentation.toGenerators
                        (Algebra.PreSubmersivePresentation.toPresentation
                          (universalFactorizationMapPresentation R n m k hn))))) :
                MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+*
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)) :
                MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) :
            (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (((↑Algebra.TensorProduct.includeRight :
              MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
            (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ Eq (α := MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(aeval
            (Algebra.Generators.val
              (Algebra.Presentation.toGenerators
                (Algebra.PreSubmersivePresentation.toPresentation
                  (universalFactorizationMapPresentation R n m k hn))))) :
        MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)) :
        MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
    (↑Algebra.TensorProduct.includeRight :
      MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
ext