awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n_1 : ℕ
⊢ 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_1 =
    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_1

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
n_1 : ℕ
⊢ 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_1 =
    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_1

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
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 }
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])
| (↑p : S[X])

Tactic:
rw [← (Equiv.eq_symm_apply _).mp f.2]

Premises used: Iff.mp, Subtype.property, Equiv.eq_symm_apply
-- 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
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 }
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])
⊢ 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])

Tactic:
conv_rhs => rw [← (Equiv.eq_symm_apply _).mp f.2]

Premises used: Iff.mp, Subtype.property, Equiv.eq_symm_apply
-- 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
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]) =
    (↑((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:
simp [MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.universalFactorizationMap]

Premises used: MvPolynomial.universalFactorizationMap, MvPolynomial.coe_mapEquivMonic_comp
-- 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
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)

Tactic:
(mapEquivMonic R S n).eq_symm_apply.mpr <| Subtype.ext ?_

Premises used: Iff.mpr, MvPolynomial.mapEquivMonic, Equiv.eq_symm_apply, Subtype.ext
-- 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
p : MonicDegreeEq S n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }
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)
                ⋯ :
              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])
⊢ 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)

Tactic:
refine (mapEquivMonic R S n).eq_symm_apply.mpr <| Subtype.ext ?_

Premises used: Iff.mpr, MvPolynomial.mapEquivMonic, Equiv.eq_symm_apply, Subtype.ext
-- 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
p : MonicDegreeEq S n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }
⊢ HMul.hMul (α := S[X])
      (Polynomial.map
        (↑(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) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S)
        (↑((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]))
      (Polynomial.map
        (↑(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) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S)
        (↑((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])) =
    (↑p : S[X])

Tactic:
simp [← coe_mapEquivMonic_comp, ← q.2]

Premises used: Subtype.property, MvPolynomial.coe_mapEquivMonic_comp
-- 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)
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:
aesop
-- 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)
⊢ ∀ (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
-- 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)
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
⊢ 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:
simp_all only [RingHom.mem_ker, map_zero, sub_zero]

Premises used: sub_zero, RingHom.mem_ker, map_zero
-- 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 : R
⊢ Membership.mem (γ := 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))))
    (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))
          ((C : (a : R) → MvPolynomial (Fin n) R) a) :
        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)
            ((f :
                (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              ((C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
                ((C : (a : R) → MvPolynomial (Fin n) R) a)))) :
        MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))

Tactic:
simp [f]
-- 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),
    (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)))
⊢ 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)

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]

Premises used: Ideal.span_le, map_sub, sub_eq_zero, RingHom.coe_coe, RingHom.mem_ker, MvPolynomial.coe_eval₂Hom, MvPolynomial.eval₂Hom_map_hom, SetLike.mem_coe, Set.range_subset_iff, MvPolynomial.eval₂Hom_C