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
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' :
  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)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (map (algebraMap ℤ R)))
      ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i ⊗ₜ[ℤ] 1))
      p)
    ((F.toRingHom :
        (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      0)

Tactic:
rw [Polynomial.hom_eval₂, ← MvPolynomial.universalFactorizationMap_comp_map] at hp'

Premises used: MvPolynomial.universalFactorizationMap_comp_map, Polynomial.hom_eval₂
-- 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' :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (map (algebraMap ℤ R)))
      ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i ⊗ₜ[ℤ] 1))
      p)
    ((F.toRingHom :
        (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      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

Tactic:
simpa [← Polynomial.eval₂_map, F] using hp'

Premises used: Polynomial.eval₂_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),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)

Tactic:
have H₁ (i : _) : (universalFactorizationMap R n m k hn).IsIntegralElem (.X i ⊗ₜ 1) := by
    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
    refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩
    apply_fun F.toRingHom at hp'
    rw [Polynomial.hom_eval₂, ← MvPolynomial.universalFactorizationMap_comp_map] at hp'
    simpa [← Polynomial.eval₂_map, F] using hp'
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
obtain :
  ∀ (p : (MvPolynomial (Fin n) ℤ)[X]) (hp : p.Monic)
    (hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (1 ⊗ₜ[ℤ] X i) p = 0),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] X i)
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (1 ⊗ₜ[R] X i)

Tactic:
obtain ⟨p, hp, hp'⟩ : (universalFactorizationMap ℤ n m k hn).IsIntegralElem (1 ⊗ₜ .X i) := by
      simpa [coeff_freeMonic] using Polynomial.isIntegral_coeff_of_dvd _ _ (monic_freeMonic _ _)
        ((monic_freeMonic _ _).map _)
        ⟨_, (universalFactorizationMap_freeMonic ℤ n m k hn).trans (mul_comm _ _)⟩ 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (1 ⊗ₜ[ℤ] X i) p = 0
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (1 ⊗ₜ[R] X i)

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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (1 ⊗ₜ[ℤ] X i) p = 0
refine :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p))
    0
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (1 ⊗ₜ[R] X i)

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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap ℤ n m k hn)) (1 ⊗ₜ[ℤ] X i) 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)) (1 ⊗ₜ[ℤ] X i) 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
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
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)) (1 ⊗ₜ[ℤ] X i) 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)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (map (algebraMap ℤ R)))
      ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (1 ⊗ₜ[ℤ] X i))
      p)
    ((F.toRingHom :
        (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      0)

Tactic:
rw [Polynomial.hom_eval₂, ← MvPolynomial.universalFactorizationMap_comp_map] at hp'

Premises used: MvPolynomial.universalFactorizationMap_comp_map, Polynomial.hom_eval₂
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (map (algebraMap ℤ R)))
      ((F.toRingHom :
          (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (1 ⊗ₜ[ℤ] X i))
      p)
    ((F.toRingHom :
        (a : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      0)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p))
    0

Tactic:
simpa [← Polynomial.eval₂_map, F] using hp'

Premises used: Polynomial.eval₂_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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
⊢ ∀ (i : Fin k),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] X i)

Tactic:
have H₂ (i : _) : (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ .X i) := by
    obtain ⟨p, hp, hp'⟩ : (universalFactorizationMap ℤ n m k hn).IsIntegralElem (1 ⊗ₜ .X i) := by
      simpa [coeff_freeMonic] using Polynomial.isIntegral_coeff_of_dvd _ _ (monic_freeMonic _ _)
        ((monic_freeMonic _ _).map _)
        ⟨_, (universalFactorizationMap_freeMonic ℤ n m k hn).trans (mul_comm _ _)⟩ i
    refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩
    apply_fun F.toRingHom at hp'
    rw [Polynomial.hom_eval₂, ← MvPolynomial.universalFactorizationMap_comp_map] at hp'
    simpa [← Polynomial.eval₂_map, F] using hp'
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
H₂ :
  ∀ (i : Fin k),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] X i)
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) 0

Tactic:
RingHom.isIntegralElem_zero _

Premises used: RingHom.isIntegralElem_zero
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
H₂ :
  ∀ (i : Fin k),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] X i)
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) 0

Tactic:
exact RingHom.isIntegralElem_zero _

Premises used: RingHom.isIntegralElem_zero
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
H₂ :
  ∀ (i : Fin k),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] X i)
x y : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
h : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) x
h_1 : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) y
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x + y)

Tactic:
RingHom.IsIntegralElem.add _ ‹_› ‹_›

Premises used: RingHom.IsIntegralElem.add, Quotient, TensorProduct, AddCon.Quotient