awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ LE.le (α := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
    (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))))
    (RingHom.ker f)
have a : ∀ (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 [Ideal.span_le, Set.range_subset_iff, SetLike.mem_coe, RingHom.mem_ker, map_sub,
      eval₂Hom_C, RingHom.coe_coe, eval₂Hom_map_hom, coe_eval₂Hom, sub_eq_zero, f]
-- 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
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)
⊢ ∀ (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)))
have 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)
Tactic: simp only [← algebraMap_eq, AlgHom.comp_algebraMap_of_tower, ← aeval_def]
-- 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
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
⊢ 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)
have 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)
Tactic: generalize universalFactorizationMap R n m k hn (X i) = p
-- 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
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
⊢ 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)
have 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)
Tactic: change AlgHom.id R _ p = ((aeval _).comp (tensorEquivSum R _ _ R).toAlgHom) p
-- 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
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
⊢ 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)
have 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))
Tactic: congr 1
-- 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
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
⊢ 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))
have a : ∀ (i : 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) :
      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) :
      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ (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
have 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)
Tactic: change ((aeval _).restrictScalars R |>.comp (mapAlgHom (Algebra.ofId _ _)) |>.comp
          (tensorEquivSum R (Fin m) (Fin k) R).toAlgHom) s = AlgHom.id R _ s
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ 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)
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ 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))
have e_a : ∀ (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: ext
-- 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
i : Fin m
j : Fin n
⊢ Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl i) : (a : MvPolynomial (Fin m ⊕ Fin k) R) → 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)
          ((universalFactorizationMap R n m k hn :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X j))) :
      MvPolynomial (Fin m ⊕ Fin k) R)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
      else
        if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
have trans : Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
  ((pderiv (Sum.inl i) : (a : MvPolynomial (Fin m ⊕ Fin k) R) → 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)
        ((universalFactorizationMap R n m k hn :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X j))) :
    MvPolynomial (Fin m ⊕ Fin k) R)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0 :
    MvPolynomial (Fin m ⊕ Fin k) R)
Tactic: trans ∑ x ∈ Finset.antidiagonal ↑j,
    if h : x.2 < k then if x.1 < m ∧ x.1 = ↑i then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = ↑i then 1 else 0