awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
p : MonicDegreeEq S n
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
rw :
  Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (↑(IsScalarTower.toAlgHom R S T) : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
rw₁ rw₂ :
  Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (AlgHom.comp (IsScalarTower.toAlgHom R S T)
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p) :
      MvPolynomial (Fin n) R →ₐ[R] T)

Tactic:
rw [← mapEquivMonic_symm_map, IsScalarTower.coe_toAlgHom]

Premises used: IsScalarTower.coe_toAlgHom, MvPolynomial.mapEquivMonic_symm_map
-- 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_1 hn : n = m + k
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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_1 hn : n = m + k
h : Nontrivial R
⊢ Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
nontriviality MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R

Premises used: MvPolynomial, Fin
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                    (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                  Algebra.TensorProduct.includeLeft) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                    (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
        n =
      1 ∧
    ∀ i > n,
      (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                      (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                    Algebra.TensorProduct.includeLeft) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                      (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                    Algebra.TensorProduct.includeRight) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
          i =
        0

Tactic:
(MonicDegreeEq.mk _ ?_ ?_).2

Premises used: Polynomial.MonicDegreeEq.mk, Subtype.property
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).Monic

Tactic:
((monic_freeMonic R m).map _).mul ((monic_freeMonic R _).map _)

Premises used: Polynomial.monic_freeMonic, Polynomial.map, Polynomial.Monic.map, Polynomial.Monic.mul, Polynomial.freeMonic
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).Monic

Tactic:
exact ((monic_freeMonic R m).map _).mul ((monic_freeMonic R _).map _)

Premises used: Polynomial.monic_freeMonic, Polynomial.Monic.map, Polynomial.Monic.mul
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
refine_2 :
  (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m))
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k))).natDegree =
    n
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
              Algebra.TensorProduct.includeLeft) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
              Algebra.TensorProduct.includeRight) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).natDegree =
    n

Tactic:
dsimp [mapEquivMonic]

Premises used: MvPolynomial.mapEquivMonic
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
refine_2 :
  natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m)) +
      natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k)) =
    n
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m))
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k))).natDegree =
    n

Tactic:
rw [((monic_freeMonic R m).map _).natDegree_mul ((monic_freeMonic R k).map _)]

Premises used: Polynomial.monic_freeMonic, Polynomial.Monic.natDegree_mul, Polynomial.Monic.map
-- 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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
refine_2 :
  natDegree (R := MvPolynomial (Fin m) R) (freeMonic R m) + natDegree (R := MvPolynomial (Fin k) R) (freeMonic R k) = n
refine_2₁ : m + k = n
⊢ natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m)) +
      natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k)) =
    n

Tactic:
simp_rw [(monic_freeMonic R _).natDegree_map, natDegree_freeMonic, hn]

Premises used: Polynomial.Monic.natDegree_map, Polynomial.monic_freeMonic, Polynomial.natDegree_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
change :
  (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n :
            (a : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
              MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n)
          (universalFactorizationMap R n m k hn)) :
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (freeMonic R m))
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
⊢ Polynomial.map
      (↑(universalFactorizationMap R n m k hn) :
        MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (freeMonic R n) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (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:
change (mapEquivMonic _ _ _ (universalFactorizationMap R n m k hn)).1 = _

Premises used: MvPolynomial.universalFactorizationMap, MvPolynomial.mapEquivMonic, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
simp :
  HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (freeMonic R m))
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n :
            (a : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
              MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n)
          (universalFactorizationMap R n m k hn)) :
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (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:
simp [universalFactorizationMap]

Premises used: MvPolynomial.universalFactorizationMap
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
⊢ HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (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:
rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
x : R
⊢ Eq.{u_2 + 1} (α := MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
    (((RingHom.comp (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap S n m k hn)) (map (algebraMap R S))) C :
            RingHom.{u_1, u_2} R (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
          (a : R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        x :
      MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
    (((RingHom.comp
              (RingHom.comp
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift
                      (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                      (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                        (mapAlgHom (Algebra.ofId R S)))
                      ⋯ :
                    AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)))
                (AlgHom.toRingHom (universalFactorizationMap R n m k hn)))
              C :
            RingHom.{u_1, u_2} R (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
          (a : R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        x :
      MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
i : Fin n
hX :
  ∀ (n : ℕ),
    Polynomial.coeff
        (Polynomial.map (R := MvPolynomial (Fin m) R)
          (RingHom.comp
            (↑Algebra.TensorProduct.includeLeft :
              MvPolynomial (Fin m) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
            (map (algebraMap R S)))
          (freeMonic R m))
        n =
      Polynomial.coeff
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                    (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                      (mapAlgHom (Algebra.ofId R S)))
                    ⋯ :
                  AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                    (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
            (↑Algebra.TensorProduct.includeLeft :
              MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
          (freeMonic R m))
        n
⊢ Eq (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
    (Polynomial.map (R := MvPolynomial (Fin m) R)
      (RingHom.comp
        (↑Algebra.TensorProduct.includeLeft :
          MvPolynomial (Fin m) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        (map (algebraMap R S)))
      (freeMonic R m))
    (Polynomial.map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                  (mapAlgHom (Algebra.ofId R S)))
                ⋯ :
              AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        (↑Algebra.TensorProduct.includeLeft :
          MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
      (freeMonic R m))

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
i : Fin n
hX :
  ∀ (n : ℕ),
    Polynomial.coeff
        (Polynomial.map (R := MvPolynomial (Fin k) R)
          (RingHom.comp
            (↑Algebra.TensorProduct.includeRight :
              MvPolynomial (Fin k) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
            (map (algebraMap R S)))
          (freeMonic R k))
        n =
      Polynomial.coeff
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                    (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                      (mapAlgHom (Algebra.ofId R S)))
                    ⋯ :
                  AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                    (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
            (↑Algebra.TensorProduct.includeRight :
              MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
          (freeMonic R k))
        n
⊢ Eq (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
    (Polynomial.map (R := MvPolynomial (Fin k) R)
      (RingHom.comp
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        (map (algebraMap R S)))
      (freeMonic R k))
    (Polynomial.map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                  (mapAlgHom (Algebra.ofId R S)))
                ⋯ :
              AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
      (freeMonic R k))

Tactic:
ext