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))) ⋯
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:
exact RingHom.IsIntegralElem.add _ ‹_› ‹_›

Premises used: RingHom.IsIntegralElem.add
-- 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_3 : 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
this :
  RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (HMul.hMul (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y))
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] y)

Tactic:
simpa
-- 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
tmul :
  RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (HMul.hMul (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y))
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] y)

Tactic:
suffices (universalFactorizationMap R n m k hn).IsIntegralElem (x ⊗ₜ 1 * 1 ⊗ₜ y) by simpa
-- 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (HMul.hMul (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y))

Tactic:
RingHom.IsIntegralElem.mul _ ?_ ?_

Premises used: RingHom.IsIntegralElem.mul
-- 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
tmul : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] 1)
tmul₁ : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] y)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (HMul.hMul (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y))

Tactic:
refine RingHom.IsIntegralElem.mul _ ?_ ?_

Premises used: RingHom.IsIntegralElem.mul
-- 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)
y : MvPolynomial (Fin k) R
a : R
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    ((C : (a : R) → MvPolynomial (Fin m) R) a ⊗ₜ[R] 1)

Tactic:
simpa using (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)

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

Tactic:
simp only [TensorProduct.add_tmul, RingHom.IsIntegralElem.add, *]

Premises used: RingHom.IsIntegralElem.add, TensorProduct.add_tmul
-- 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)
y : MvPolynomial (Fin k) R
p : MvPolynomial (Fin m) R
i : Fin m
IH : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (p ⊗ₜ[R] 1)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) ((p * X i) ⊗ₜ[R] 1)

Tactic:
simpa [← map_mul] using IH.mul _ (H₁ i)

Premises used: map_mul, RingHom.IsIntegralElem.mul
-- 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
tmul :
  ∀ (a : R),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      ((C : (a : R) → MvPolynomial (Fin m) R) a ⊗ₜ[R] 1)
tmul₁ :
  ∀ (p q : MvPolynomial (Fin m) R),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (p ⊗ₜ[R] 1) →
      RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (q ⊗ₜ[R] 1) →
        RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) ((p + q) ⊗ₜ[R] 1)
tmul₂ :
  ∀ (p : MvPolynomial (Fin m) R) (i : Fin m)
    (IH : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (p ⊗ₜ[R] 1)),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) ((p * X i) ⊗ₜ[R] 1)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] 1)

Tactic:
induction x using MvPolynomial.induction_on with
      | C a => simpa using (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)
      | add p q _ _ => simp only [TensorProduct.add_tmul, RingHom.IsIntegralElem.add, *]
      | mul_X p i IH => simpa [← map_mul] using IH.mul _ (H₁ i)

Premises used: RingHom.IsIntegralElem.add, MvPolynomial.induction_on, map_mul, TensorProduct.add_tmul, MvPolynomial.C
-- 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 : MvPolynomial (Fin m) R
a : R
⊢ RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
    (1 ⊗ₜ[R] (C : (a : R) → MvPolynomial (Fin k) R) a)

Tactic:
simpa [← algebraMap_eq, ← algebraMap_apply, Algebra.algebraMap_eq_smul_one] using
          (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)

Premises used: RingHom.isIntegralElem_map, MvPolynomial.algebraMap_apply, Algebra.algebraMap_eq_smul_one, MvPolynomial.universalFactorizationMap, AlgHom.toRingHom, MvPolynomial.algebraMap_eq
-- 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 : MvPolynomial (Fin m) R
p q : MvPolynomial (Fin k) R
h : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] p)
h_1 : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] q)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] (p + q))

Tactic:
simp only [TensorProduct.tmul_add, RingHom.IsIntegralElem.add, *]

Premises used: RingHom.IsIntegralElem.add, TensorProduct.tmul_add
-- 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 : MvPolynomial (Fin m) R
p : MvPolynomial (Fin k) R
i : Fin k
IH : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] p)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] (p * X i))

Tactic:
simpa [← map_mul] using IH.mul _ (H₂ i)

Premises used: map_mul, RingHom.IsIntegralElem.mul
-- 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 : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
tmul :
  ∀ (a : R),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (1 ⊗ₜ[R] (C : (a : R) → MvPolynomial (Fin k) R) a)
tmul₁ :
  ∀ (p q : MvPolynomial (Fin k) R),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] p) →
      RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] q) →
        RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] (p + q))
tmul₂ :
  ∀ (p : MvPolynomial (Fin k) R) (i : Fin k)
    (IH : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] p)),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] (p * X i))
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] y)

Tactic:
induction y using MvPolynomial.induction_on with
      | C a => simpa [← algebraMap_eq, ← algebraMap_apply, Algebra.algebraMap_eq_smul_one] using
          (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)
      | add p q _ _ => simp only [TensorProduct.tmul_add, RingHom.IsIntegralElem.add, *]
      | mul_X p i IH => simpa [← map_mul] using IH.mul _ (H₂ i)

Premises used: RingHom.IsIntegralElem.add, MvPolynomial.algebraMap_apply, MvPolynomial.induction_on, Algebra.algebraMap_eq_smul_one, map_mul, MvPolynomial.algebraMap_eq, TensorProduct.tmul_add, MvPolynomial.C
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ Eq (α := 𝓡) (coeff (map (algebraMap R 𝓡) (↑p : R[X])) n) 1 ∧
    ∀ i > n, Eq (α := 𝓡) (coeff (map (algebraMap R 𝓡) (↑p : R[X])) i) 0

Tactic:
simp +contextual only [Polynomial.coeff_map, p.2,
    map_one, map_zero, gt_iff_lt, implies_true, and_self]

Premises used: Polynomial.coeff_map, and_self, map_zero, map_one, gt_iff_lt, implies_true, Subtype.property