awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
inl :
  Subsingleton R →
    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))
⊢ 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))
have inr : Nontrivial R →
  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: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ 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))
have 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 sorry) (finCongr sorry) :
              (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))
Tactic: rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det,
    MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ resultant
      (Polynomial.map
        (@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)))
        (freeMonic R m))
      (Polynomial.map
        (@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)))
        (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))
have inr : @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)) =
  Algebra.TensorProduct.includeLeftRingHom
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ @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)) =
    Algebra.TensorProduct.includeLeftRingHom
have 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.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: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ m =
    natDegree (R := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
have inr : m = natDegree (R := MvPolynomial (Fin m) R) (freeMonic R m)
Tactic: rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ m =
    natDegree (R := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
have inr₁ : m = m
Tactic: rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ k =
    natDegree
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
have inr : k = natDegree (R := MvPolynomial (Fin k) R) (freeMonic R k)
Tactic: rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ k =
    natDegree
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
have inr₁ : k = k
Tactic: rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
have refine : RingHom.IsIntegral (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
Tactic: refine RingHom.IsIntegral.to_finite ?_
    (.of_finitePresentation (finitePresentation_universalFactorizationMap R n m k hn))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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))
⊢ RingHom.IsIntegral (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (X i ⊗ₜ[R] 1)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
have 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
Tactic: refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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)
    (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p))
    0
have hp'₁ : 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'
Cleared hypotheses: hp'