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
⊢ (↑((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))
have 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))
Tactic: simp [universalFactorizationMap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ Eq (α := RingHom.{u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S))
    (RingHom.comp (AlgHom.toRingHom (universalFactorizationMap S n m k hn)) (map (algebraMap R S)))
    (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)))
have hC : ∀ (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)))
                      sorry :
                    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: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ 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))
have 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)))
                  sorry :
                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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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
⊢ 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))
have 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)))
                  sorry :
                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
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
p : MonicDegreeEq S n
f :
  { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
    f.comp (universalFactorizationMap R n m k hn) =
      (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }
| (↑p : S[X])
have rw : (↑((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n)
      ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp (universalFactorizationMap R n m k hn))) :
  S[X])
Tactic: rw [← (Equiv.eq_symm_apply _).mp f.2]
-- 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
p : MonicDegreeEq S n
f :
  { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
    f.comp (universalFactorizationMap R n m k hn) =
      (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }
⊢ HMul.hMul (α := S[X])
      (↑((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeLeft),
              (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeRight)).1 :
        S[X])
      (↑((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeLeft),
              (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeRight)).2 :
        S[X]) =
    (↑p : S[X])
have conv_rhs : HMul.hMul (α := S[X])
    (↑((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
              ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                Algebra.TensorProduct.includeLeft),
            (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
              ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                Algebra.TensorProduct.includeRight)).1 :
      S[X])
    (↑((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
              ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                Algebra.TensorProduct.includeLeft),
            (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
              ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                Algebra.TensorProduct.includeRight)).2 :
      S[X]) =
  (↑((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n)
        ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
          (universalFactorizationMap R n m k hn))) :
    S[X])
Tactic: conv_rhs => rw [← (Equiv.eq_symm_apply _).mp f.2]
-- 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
p : MonicDegreeEq S n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] S)
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
            (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
          ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
            (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
          ⋯ :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S)
      (universalFactorizationMap R n m k hn :
        MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
    ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p)
have refine : (↑((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n)
        (AlgHom.comp
          (Algebra.TensorProduct.lift
              ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
              ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
              sorry :
            MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S)
          (universalFactorizationMap R n m k hn :
            MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))) :
    S[X]) =
  (↑p : S[X])
Tactic: refine (mapEquivMonic R S n).eq_symm_apply.mpr <| Subtype.ext ?_
-- 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
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)
⊢ Eq (α := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) (RingHom.ker f)
    (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))))
have 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)
Tactic: have H (i : _) : tensorEquivSum _ _ _ _ (f (.X i)) = .X i := by aesop
-- 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)
⊢ Eq (α := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) (RingHom.ker f)
    (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))))
have a : LE.le (α := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) (RingHom.ker f)
  (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))))
Tactic: apply le_antisymm
-- 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)
x : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
hx :
  Membership.mem (γ :=
    Submodule (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
      (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
    (RingHom.ker f) x
⊢ Membership.mem (γ :=
    Submodule (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
      (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))))
    x
have h : x =
  HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) x
    ((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 :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            x)) :
      MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
Tactic: convert_to x - (tensorEquivSum _ _ _ _ (f x)).map C ∈ Ideal.span _ using 1