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
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
a :
  ∀ (y : Fin n),
    Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((universalFactorizationMap R n m k hn :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X y) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x) :
            (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          ((tensorEquivSum R (Fin m) (Fin k) R :
              (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
            ((universalFactorizationMap R n m k hn :
                (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (X y))) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ ∀ (y : Fin n),
    (universalFactorizationMap R n m k hn :
          (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X y) =
      eval₂ (σ := Fin m ⊕ Fin k)
        (RingHom.comp
          (↑(universalFactorizationMap R n m k hn) :
            MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          C)
        (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((universalFactorizationMap R n m k hn :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X y)))

Tactic:
simp only [← algebraMap_eq, AlgHom.comp_algebraMap_of_tower, ← aeval_def]

Premises used: AlgHom.comp_algebraMap_of_tower, MvPolynomial.aeval_def, MvPolynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
a :
  ∀ (p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R),
    p =
      (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x) :
          (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          p)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((universalFactorizationMap R n m k hn :
          (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x) :
          (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((universalFactorizationMap R n m k hn :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i))) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
generalize universalFactorizationMap R n m k hn (X i) = p

Premises used: MvPolynomial.X, MvPolynomial.universalFactorizationMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
a :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        p :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
            (↑(tensorEquivSum R (Fin m) (Fin k) R) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        p :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ p =
    (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x) :
        (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
        p)

Tactic:
change AlgHom.id R _ p = ((aeval _).comp (tensorEquivSum R _ _ R).toAlgHom) p

Premises used: MvPolynomial.aeval, AlgEquiv.toAlgHom, MvPolynomial.tensorEquivSum, AlgHom.id, AlgHom.comp, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
a :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
    (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
      (↑(tensorEquivSum R (Fin m) (Fin k) R) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        p :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
            (↑(tensorEquivSum R (Fin m) (Fin k) R) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        p :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i_1 : Fin m
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i_1) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
              (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
            Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i_1) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i_1 : Fin k
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i_1) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (AlgHom.restrictScalars R
              (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
                (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i_1) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
change :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp
            (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              (AlgHom.restrictScalars R
                (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
              (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
            (↑(tensorEquivSum R (Fin m) (Fin k) R) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        s :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        s :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x) :
        (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          s)) =
    s

Tactic:
change ((aeval _).restrictScalars R |>.comp (mapAlgHom (Algebra.ofId _ _)) |>.comp
          (tensorEquivSum R (Fin m) (Fin k) R).toAlgHom) s = AlgHom.id R _ s

Premises used: MvPolynomial.aeval, AlgEquiv.toAlgHom, MvPolynomial.tensorEquivSum, AlgHom.id, MvPolynomial.mapAlgHom, Algebra.ofId, AlgHom.restrictScalars, AlgHom.comp, Fin, DFunLike.coe
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
e_a :
  Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (AlgHom.comp
      (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
        (AlgHom.restrictScalars R (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
        (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
      (↑(tensorEquivSum R (Fin m) (Fin k) R) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
    (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp
            (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              (AlgHom.restrictScalars R
                (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
              (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
            (↑(tensorEquivSum R (Fin m) (Fin k) R) :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        s :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        s :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
congr 1
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i : Fin m
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (AlgHom.comp
              (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
                (AlgHom.restrictScalars R
                  (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
                (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
              (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
            Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i : Fin k
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (AlgHom.restrictScalars R
              (AlgHom.comp
                (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
                  (AlgHom.restrictScalars R
                    (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
                  (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
                (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (X i) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
simp
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
⊢ Eq.{max (u_1 + 1) 1} (α :=
    Ideal
      (Algebra.Generators.Ring (R := MvPolynomial (Fin n) R) (S := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (ι := Fin m ⊕ Fin k)
        { val := Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x,
          σ' := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) ↦
            (map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              ((tensorEquivSum R (Fin m) (Fin k) R :
                  (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
                f),
          aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }))
    (Ideal.span
      (Set.range fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (β :=
          MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
          ((C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (X i) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
          ((map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              ((tensorEquivSum R (Fin m) (Fin k) R :
                  (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
                ((universalFactorizationMap R n m k hn :
                    (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                  (X i))) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))))
    (Algebra.Generators.ker
      { val := Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x,
        σ' := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) ↦
          (map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
            ((tensorEquivSum R (Fin m) (Fin k) R :
                (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
              f),
        aeval_val_σ' := ⋯, algebraMap_eq := ⋯ })

Tactic:
(ker_eval₂Hom_universalFactorizationMap R n m k hn).symm

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, MonoidHomClass.toMonoidHom, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, RingHomClass.toRingHom, AddMonoidAlgebra, Eq.symm, Finset.sum