awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' :
  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₂ (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)
  (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'
Cleared hypotheses: hp'
-- 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))) ⋯
⊢ RingHom.IsIntegral (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
have H₁ : ∀ (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'
-- 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))) ⋯
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)
have 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)
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
-- 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))) ⋯
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)
have 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
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))) ⋯
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)
    (Polynomial.eval₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] X i)
      (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)) (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'
Cleared hypotheses: hp'
-- 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))) ⋯
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₂ (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p))
    0
have 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)
Tactic: rw [Polynomial.hom_eval₂, ← MvPolynomial.universalFactorizationMap_comp_map] at hp'
Cleared hypotheses: hp'
-- 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))) ⋯
H₁ :
  ∀ (i : Fin m),
    RingHom.IsIntegralElem (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
      (X i ⊗ₜ[R] 1)
⊢ RingHom.IsIntegral (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
have H₂ : ∀ (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'
-- 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))) ⋯
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)) (x ⊗ₜ[R] y)
have 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))
Tactic: suffices (universalFactorizationMap R n m k hn).IsIntegralElem (x ⊗ₜ 1 * 1 ⊗ₜ y) by simpa
-- 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))) ⋯
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))
have tmul : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] 1)
Tactic: refine RingHom.IsIntegralElem.mul _ ?_ ?_
-- 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))) ⋯
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)
⊢ 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))
have tmul₁ : RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (1 ⊗ₜ[R] y)
Tactic: refine RingHom.IsIntegralElem.mul _ ?_ ?_
-- 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))) ⋯
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)) (x ⊗ₜ[R] 1)
have 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)
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)
Cleared hypotheses: x
-- 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))) ⋯
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)
⊢ RingHom.IsIntegralElem (AlgHom.toRingHom (universalFactorizationMap R n m k hn)) (x ⊗ₜ[R] 1)
have 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)
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)
Cleared hypotheses: x