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
p : MonicDegreeEq R n
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    AlgHom.comp (Algebra.ofId R 𝓡)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p)

Tactic:
AlgHom.ext fun x ↦ (Algebra.TensorProduct.tmul_one_eq_one_tmul x).symm

Premises used: AlgHom.ext, Algebra.TensorProduct.tmul_one_eq_one_tmul, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    AlgHom.comp (Algebra.ofId R 𝓡)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p)

Tactic:
exact AlgHom.ext fun x ↦ (Algebra.TensorProduct.tmul_one_eq_one_tmul x).symm

Premises used: AlgHom.ext
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
rw :
  (MvPolynomial.mapEquivMonic R 𝓡 n : (a : MvPolynomial (Fin n) R →ₐ[R] 𝓡) → MonicDegreeEq 𝓡 n)
      (AlgHom.comp (Algebra.ofId R 𝓡)
        ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
          p)) =
    monicDegreeEq m k hn p
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Equiv.symm (MvPolynomial.mapEquivMonic R 𝓡 n) : (a : MonicDegreeEq 𝓡 n) → MvPolynomial (Fin n) R →ₐ[R] 𝓡)
      (monicDegreeEq m k hn p)

Tactic:
rw [UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
a :
  (↑((MvPolynomial.mapEquivMonic R 𝓡 n : (a : MvPolynomial (Fin n) R →ₐ[R] 𝓡) → MonicDegreeEq 𝓡 n)
          (AlgHom.comp (Algebra.ofId R 𝓡)
            ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
              p))) :
      𝓡[X]) =
    (↑(monicDegreeEq m k hn p) : 𝓡[X])
⊢ (MvPolynomial.mapEquivMonic R 𝓡 n : (a : MvPolynomial (Fin n) R →ₐ[R] 𝓡) → MonicDegreeEq 𝓡 n)
      (AlgHom.comp (Algebra.ofId R 𝓡)
        ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
          p)) =
    monicDegreeEq m k hn p

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (↑((MvPolynomial.mapEquivMonic R 𝓡 n : (a : MvPolynomial (Fin n) R →ₐ[R] 𝓡) → MonicDegreeEq 𝓡 n)
          (AlgHom.comp (Algebra.ofId R 𝓡)
            ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
              p))) :
      𝓡[X]) =
    (↑(monicDegreeEq m k hn p) : 𝓡[X])

Tactic:
simp [MvPolynomial.coe_mapEquivMonic_comp, monicDegreeEq]

Premises used: Polynomial.UniversalFactorizationRing.monicDegreeEq, MvPolynomial.coe_mapEquivMonic_comp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (↑(factor₁ m k hn p) : 𝓡[X]) * (↑(factor₂ m k hn p) : 𝓡[X]) = (↑(monicDegreeEq m k hn p) : 𝓡[X])

Tactic:
(MvPolynomial.universalFactorizationMapLiftEquiv _ _ n m k hn _
    ⟨fromTensor m k hn p, fromTensor_comp_universalFactorizationMap' m k hn p⟩).2

Premises used: MvPolynomial.universalFactorizationMapLiftEquiv, Subtype.mk, Polynomial.UniversalFactorizationRing.fromTensor, DFunLike.coe, Subtype.property, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'
-- 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 R n
f : 𝓡 →ₐ[R] S
⊢ HMul.hMul (α := S[X]) (↑((factor₁ m k hn p).map (↑f : 𝓡 →+* S), (factor₂ m k hn p).map (↑f : 𝓡 →+* S)).1 : S[X])
      (↑((factor₁ m k hn p).map (↑f : 𝓡 →+* S), (factor₂ m k hn p).map (↑f : 𝓡 →+* S)).2 : S[X]) =
    map (algebraMap R S) (↑p : R[X])

Tactic:
simp [← Polynomial.map_mul, factor₁_mul_factor₂ m k hn p, Polynomial.map_map]

Premises used: Polynomial.map_mul, Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this : IsScalarTower (MvPolynomial (Fin n) R) R S
f : { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
  f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Equiv.symm (MvPolynomial.mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
      (p.map (algebraMap R S)) } :=
  (Equiv.symm (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑(p.map (algebraMap R S)) : S[X]) }) →
        { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
          f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
            ((MvPolynomial.mapEquivMonic R S n).symm : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
              (p.map (algebraMap R S)) })
    q
r : MvPolynomial (Fin n) R
simp :
  Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
                  p :
                MvPolynomial (Fin n) R →ₐ[R] R) :
              (a : MvPolynomial (Fin n) R) → R)
            r :
          R) :
      S)
    ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S) r : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((((Equiv.symm (MvPolynomial.mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
              (p.map (algebraMap R S)) :
            MvPolynomial (Fin n) R →ₐ[R] S) :
          (a : MvPolynomial (Fin n) R) → S)
        r :
      S)
    ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S) r : S)

Tactic:
simp [MvPolynomial.mapEquivMonic_symm_map_algebraMap]

Premises used: MvPolynomial.mapEquivMonic_symm_map_algebraMap
-- 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 R n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this : IsScalarTower (MvPolynomial (Fin n) R) R S
f : { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
  f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Equiv.symm (MvPolynomial.mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
      (p.map (algebraMap R S)) } :=
  (Equiv.symm (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑(p.map (algebraMap R S)) : S[X]) }) →
        { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
          f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
            ((MvPolynomial.mapEquivMonic R S n).symm : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
              (p.map (algebraMap R S)) })
    q
r : MvPolynomial (Fin n) R
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R)
                  p :
                MvPolynomial (Fin n) R →ₐ[R] R) :
              (a : MvPolynomial (Fin n) R) → R)
            r :
          R) :
      S)
    ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S) r : S)

Tactic:
rfl
-- 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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
⊢ IsScalarTower (MvPolynomial (Fin n) R) R S

Tactic:
haveI : IsScalarTower (MvPolynomial (Fin n) R) R S := .of_algebraMap_eq' rfl
-- 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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this : IsScalarTower (MvPolynomial (Fin n) R) R S
r : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S)
        ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R) :
      S)

Tactic:
simp [Algebra.compHom_algebraMap_apply]

Premises used: Algebra.compHom_algebraMap_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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this : IsScalarTower (MvPolynomial (Fin n) R) R S
⊢ IsScalarTower R (MvPolynomial (Fin n) R) S

Tactic:
have : IsScalarTower R (MvPolynomial (Fin n) R) S := .of_algebraMap_eq fun r ↦ by
      simp [Algebra.compHom_algebraMap_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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_4 : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
⊢ AlgHom.comp (B := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
      ((fun
            (q :
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) ↦
          (Algebra.TensorProduct.lift (Algebra.ofId R S)
              (let __RingHom : RingHom.{u_1, u_2} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S :=
                AlgHom.toRingHom (R := R)
                  (↑((Equiv.symm
                            (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))) :
                          (a :
                              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                                (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑(p.map (algebraMap R S)) : S[X]) }) →
                            { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                              f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
                                ((MvPolynomial.mapEquivMonic R S n).symm :
                                    (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                  (p.map (algebraMap R S)) })
                        q) :
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S);
              { toRingHom := __RingHom, commutes' := ⋯ })
              ⋯ :
            R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[R] S))
        ((fun (f : 𝓡 →ₐ[R] S) ↦
            (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                ((factor₁ m k hn p).map (↑f : 𝓡 →+* S), (factor₂ m k hn p).map (↑f : 𝓡 →+* S)) ⋯ :
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }))
          f))
      Algebra.TensorProduct.includeLeft =
    f.comp Algebra.TensorProduct.includeLeft

Tactic:
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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_4 : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i : Fin m
⊢ Eq.{u_2 + 1} (α := S)
    ((f : (a : 𝓡) → S)
        ((fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
            (MvPolynomial.X i ⊗ₜ[R] 1) :
          𝓡) :
      S)
    ((f : (a : R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) → S)
        (1 ⊗ₜ[MvPolynomial (Fin n) R] (MvPolynomial.X i ⊗ₜ[R] 1)) :
      S)

Tactic:
rfl
-- 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 R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_4 : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i : Fin k
⊢ Eq.{u_2 + 1} (α := S)
    ((f : (a : 𝓡) → S)
        ((fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
            (1 ⊗ₜ[R] MvPolynomial.X i) :
          𝓡) :
      S)
    ((f : (a : R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) → S)
        (1 ⊗ₜ[MvPolynomial (Fin n) R] (1 ⊗ₜ[R] MvPolynomial.X i)) :
      S)

Tactic:
rfl
-- 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 R n
⊢ Module.Finite R 𝓡

Tactic:
letI := (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
  letI := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra
  letI : Module.Finite _ _ := MvPolynomial.finite_universalFactorizationMap R n m k hn
  inferInstanceAs (Module.Finite R (R ⊗[_] _))

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- 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 R n
⊢ Algebra.FinitePresentation R 𝓡

Tactic:
letI := (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
  letI := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra
  letI : Algebra.FinitePresentation _ _ :=
    MvPolynomial.finitePresentation_universalFactorizationMap R n m k hn
  inferInstanceAs (Algebra.FinitePresentation R (R ⊗[_] _))

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
inl :
  Subsingleton.{u_1 + 1} 𝓡 →
    (presentation m k hn p).jacobian =
      HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
inr :
  Nontrivial.{u_1} 𝓡 →
    (presentation m k hn p).jacobian =
      HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
cases subsingleton_or_nontrivial 𝓡
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : Subsingleton.{u_1 + 1} 𝓡
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : Subsingleton.{u_1 + 1} 𝓡
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : Nontrivial.{u_1} 𝓡
inr :
  Subsingleton.{u_1 + 1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
    (presentation m k hn p).jacobian =
      HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
inr₁ :
  Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
    (presentation m k hn p).jacobian =
      HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

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

Premises used: subsingleton_or_nontrivial, MvPolynomial, TensorProduct, Fin