-- 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 ⊗[R] MvPolynomial (Fin k) R
zero : RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) 0
add :
  ∀ (x y : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) x →
      RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) y →
        RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x + y)
tmul :
  ∀ (x : MvPolynomial (Fin m) R) (y : MvPolynomial (Fin k) R),
    RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] y)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) x

Tactic:
induction x with
  | zero => exact RingHom.isIntegralElem_zero _
  | add x y _ _ => exact RingHom.IsIntegralElem.add _ ‹_› ‹_›
  | tmul x y =>
    suffices (universalFactorizationMap R n m k hn).IsIntegralElem (x ⊗ₜ 1 * 1 ⊗ₜ y) by simpa
    refine RingHom.IsIntegralElem.mul _ ?_ ?_
    · 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)
    · 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, RingHom.IsIntegralElem.mul, MvPolynomial.algebraMap_eq, TensorProduct.tmul_add, TensorProduct.add_tmul, RingHom.isIntegralElem_zero, MvPolynomial.C