awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  (algebraMap
          (Algebra.Generators.Ring (R := MvPolynomial (Fin n) R)
            (Algebra.Presentation.toGenerators
              (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R n m k hn))))
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
        (a : (universalFactorizationMapPresentation R n m k hn).Ring) →
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (Matrix.det (n := Fin n)
        (-Matrix.transpose
            ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
                (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) →
                  Matrix (Fin n) (Fin n) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
              (sylvester
                (Polynomial.map (R := MvPolynomial (Fin m) R)
                  (AlgHom.toRingHom
                    (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)))
                  (freeMonic R m))
                (Polynomial.map (R := MvPolynomial (Fin k) R)
                  (AlgHom.toRingHom
                    (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)))
                  (freeMonic R k))
                m k)))) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))
⊢ Algebra.PreSubmersivePresentation.jacobian (universalFactorizationMapPresentation R n m k hn) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))

Tactic:
rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det,
    MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix]

Premises used: MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- 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 :
  (aeval
          (Algebra.Generators.val
            (Algebra.Presentation.toGenerators
              (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R n m k hn)))) :
        (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (resultant
        (Polynomial.map
          (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)) :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
          (freeMonic R m))
        (Polynomial.map
          (↑(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))
          (freeMonic R k))
        m k) =
    resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
⊢ HMul.hMul (β := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n)
      ((aeval
              (Algebra.Generators.val
                (Algebra.Presentation.toGenerators
                  (Algebra.PreSubmersivePresentation.toPresentation
                    (universalFactorizationMapPresentation R n m k hn)))) :
            (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (resultant
            (Polynomial.map
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)) :
                MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              (freeMonic R m))
            (Polynomial.map
              (↑(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))
              (freeMonic R k))
            m k) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k))

Tactic:
congr 1
-- 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))
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.inl)) :
                MvPolynomial (Fin m) 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.includeLeftRingHom C :
          (a : R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        x :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

Premises used: AddMonoidAlgebra.coe_algebraMap, MvPolynomial.algebraMap_apply, MvPolynomial.algebraMap_eq
-- 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))
i : Fin m
⊢ 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.inl)) :
              MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((Algebra.TensorProduct.includeLeftRingHom :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

Premises used: AddMonoidAlgebra.coe_algebraMap, MvPolynomial.algebraMap_apply, MvPolynomial.algebraMap_eq
-- 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))
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)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

Premises used: AddMonoidAlgebra.coe_algebraMap, MvPolynomial.algebraMap_apply, MvPolynomial.algebraMap_eq
-- 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))
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)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

Premises used: AddMonoidAlgebra.coe_algebraMap, MvPolynomial.algebraMap_apply, MvPolynomial.algebraMap_eq
-- 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 : m = natDegree (R := MvPolynomial (Fin m) R) (freeMonic R m)
inr₁ inr₂ : m = m
⊢ m =
    natDegree (R := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))

Tactic:
rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]

Premises used: Polynomial.Monic.natDegree_map, Polynomial.monic_freeMonic, Polynomial.natDegree_freeMonic
-- 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 : k = natDegree (R := MvPolynomial (Fin k) R) (freeMonic R k)
inr₁ inr₂ : k = k
⊢ k =
    natDegree
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))

Tactic:
rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]

Premises used: Polynomial.Monic.natDegree_map, Polynomial.monic_freeMonic, Polynomial.natDegree_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
⊢ AlgHom.FinitePresentation.{u_1, u_1, u_1} (R := R) (A := MvPolynomial (Fin n) R) (B :=
    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (universalFactorizationMap R n m k hn)

Tactic:
letI := (universalFactorizationMap R n m k hn).toAlgebra
  (universalFactorizationMapPresentation R n m k hn).finitePresentation_of_isFinite

Premises used: AlgHom.FinitePresentation, RingHom.FinitePresentation, Algebra.PreSubmersivePresentation.toPresentation, MvPolynomial.universalFactorizationMapPresentation, Algebra.Presentation.finitePresentation_of_isFinite
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
⊢ AlgHom.Finite (A := MvPolynomial (Fin n) R) (universalFactorizationMap R n m k hn)

Tactic:
RingHom.IsIntegral.to_finite ?_
    (.of_finitePresentation (finitePresentation_universalFactorizationMap R n m k hn))

Premises used: AlgHom.Finite, MvPolynomial.finitePresentation_universalFactorizationMap, RingHom.FiniteType.of_finitePresentation, RingHom.IsIntegral.to_finite
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
refine : RingHom.IsIntegral (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
⊢ AlgHom.Finite (A := MvPolynomial (Fin n) R) (universalFactorizationMap R n m k hn)

Tactic:
refine RingHom.IsIntegral.to_finite ?_
    (.of_finitePresentation (finitePresentation_universalFactorizationMap R n m k hn))

Premises used: MvPolynomial.finitePresentation_universalFactorizationMap, RingHom.FiniteType.of_finitePresentation, RingHom.IsIntegral.to_finite
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
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))
⊢ IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)

Tactic:
have : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
    (MvPolynomial.tensorEquivSum ℤ (Fin m) (Fin k) ℤ).toRingEquiv.isDomain_iff.mpr inferInstance
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
this_2 : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId ℤ R)))
    (AlgHom.comp (AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
⊢ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).IsIntegralElem (X i ⊗ₜ[ℤ] 1)

Tactic:
simpa [coeff_freeMonic] using Polynomial.isIntegral_coeff_of_dvd _ _ (monic_freeMonic _ _)
        ((monic_freeMonic _ _).map _) ⟨_, universalFactorizationMap_freeMonic ℤ n m k hn⟩ i

Premises used: Int, Fin.val, Polynomial.monic_freeMonic, Exists.intro, MvPolynomial.universalFactorizationMap_freeMonic, Polynomial.isIntegral_coeff_of_dvd, Polynomial.Monic.map, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
this_2 : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId ℤ R)))
    (AlgHom.comp (AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
obtain :
  ∀ (p : (MvPolynomial (Fin n) ℤ)[X]) (hp : p.Monic)
    (hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (X i ⊗ₜ[ℤ] 1) p = 0),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (X i ⊗ₜ[R] 1)

Tactic:
obtain ⟨p, hp, hp'⟩ : (universalFactorizationMap ℤ n m k hn).IsIntegralElem (.X i ⊗ₜ 1) := by
      simpa [coeff_freeMonic] using Polynomial.isIntegral_coeff_of_dvd _ _ (monic_freeMonic _ _)
        ((monic_freeMonic _ _).map _) ⟨_, universalFactorizationMap_freeMonic ℤ n m k hn⟩ i

Premises used: MvPolynomial.X, Int, RingHom.IsIntegralElem, MvPolynomial.universalFactorizationMap, AlgHom.toRingHom, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
this_2 : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId ℤ R)))
    (AlgHom.comp (AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (X i ⊗ₜ[ℤ] 1) p = 0
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (X i ⊗ₜ[R] 1)

Tactic:
⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩

Premises used: Algebra.algebraMap, Int, RingHom.IsIntegralElem, And.intro, Exists.intro, MvPolynomial.map, Polynomial.map, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
this_2 : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId ℤ R)))
    (AlgHom.comp (AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (X i ⊗ₜ[ℤ] 1) p = 0
refine :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p))
    0
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (X i ⊗ₜ[R] 1)

Tactic:
refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
this_2 : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId ℤ R)))
    (AlgHom.comp (AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (X i ⊗ₜ[ℤ] 1) p = 0
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (X i ⊗ₜ[ℤ] 1) p) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        0 :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
apply_fun F.toRingHom at hp'

Premises used: AlgHom.toRingHom