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
h : Nontrivial.{u_1} 𝓡
h_1 : Subsingleton.{u_1 + 1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (-1) n *
      (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).resultant
        (↑(factor₂ m k hn p) : (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X])
        (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree
        (↑(factor₂ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree

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 : Nontrivial.{u_1} 𝓡
h_1 : Subsingleton.{u_1 + 1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (-1) n *
      (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).resultant
        (↑(factor₂ m k hn p) : (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X])
        (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree
        (↑(factor₂ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree

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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
inr :
  Subsingleton 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 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 R

Premises used: 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 : Nontrivial.{u_1} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Subsingleton R
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (-1) n *
      (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).resultant
        (↑(factor₂ m k hn p) : (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X])
        (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree
        (↑(factor₂ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree

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 : Nontrivial.{u_1} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Subsingleton R
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (-1) n *
      (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).resultant
        (↑(factor₂ m k hn p) : (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X])
        (↑(factor₁ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree
        (↑(factor₂ m k hn p) :
            (R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))[X]).natDegree

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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
(Algebra.PreSubmersivePresentation.baseChange_jacobian _ _).trans ?_

Premises used: Algebra.PreSubmersivePresentation.baseChange_jacobian, Polynomial.UniversalFactorizationRing, Polynomial.UniversalFactorizationRing.presentation, Eq.trans
-- 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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
inr :
  1 ⊗ₜ[MvPolynomial (Fin n) R]
      Algebra.PreSubmersivePresentation.jacobian (MvPolynomial.universalFactorizationMapPresentation R n m k hn) =
    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:
refine (Algebra.PreSubmersivePresentation.baseChange_jacobian _ _).trans ?_

Premises used: Algebra.PreSubmersivePresentation.baseChange_jacobian, Eq.trans
-- 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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
inr :
  (fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
      (Algebra.PreSubmersivePresentation.jacobian (MvPolynomial.universalFactorizationMapPresentation R n m k hn)) =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
⊢ 1 ⊗ₜ[MvPolynomial (Fin n) R]
      Algebra.PreSubmersivePresentation.jacobian (MvPolynomial.universalFactorizationMapPresentation R n m k hn) =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
change fromTensor _ _ _ _ _ = _

Premises used: Polynomial.UniversalFactorizationRing.fromTensor, DFunLike.coe
-- 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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
inr :
  (fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
      (HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
        resultant (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
          (map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))) =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
⊢ (fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
      (Algebra.PreSubmersivePresentation.jacobian (MvPolynomial.universalFactorizationMapPresentation R n m k hn)) =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
rw [MvPolynomial.universalFactorizationMapPresentation_jacobian]

Premises used: MvPolynomial.universalFactorizationMapPresentation_jacobian
-- 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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
inr :
  HPow.hPow (α := 𝓡) (-1) n *
      resultant
        (map
          (RingHom.comp (↑(fromTensor m k hn p) : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* 𝓡)
            Algebra.TensorProduct.includeLeftRingHom)
          (freeMonic R m))
        (map
          (RingHom.comp (↑(fromTensor m k hn p) : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* 𝓡)
            (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
          (freeMonic R k))
        m k =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X]) m k
⊢ (fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡)
      (HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
        resultant (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
          (map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))) =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])

Tactic:
rw [map_mul, map_pow, map_neg, map_one, ← AlgHom.coe_toRingHom, ← Polynomial.resultant_map_map,
    Polynomial.map_map, Polynomial.map_map, (monic_freeMonic R k).natDegree_map,
    (monic_freeMonic R m).natDegree_map, MonicDegreeEq.natDegree,
    MonicDegreeEq.natDegree, natDegree_freeMonic, natDegree_freeMonic]

Premises used: AlgHom.coe_toRingHom, map_neg, map_pow, map_mul, Polynomial.Monic.natDegree_map, map_one, Polynomial.resultant_map_map, Polynomial.monic_freeMonic, Polynomial.natDegree_freeMonic, Polynomial.MonicDegreeEq.natDegree, Polynomial.map_map
-- 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} 𝓡
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h_2 : Nontrivial R
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))
⊢ HPow.hPow (α := 𝓡) (-1) n *
      resultant
        (map
          (RingHom.comp (↑(fromTensor m k hn p) : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* 𝓡)
            Algebra.TensorProduct.includeLeftRingHom)
          (freeMonic R m))
        (map
          (RingHom.comp (↑(fromTensor m k hn p) : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* 𝓡)
            (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
          (freeMonic R k))
        m k =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X]) m k

Tactic:
rfl
-- 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]) = (↑(p.map (algebraMap R 𝓡')) : 𝓡'[X])

Tactic:
simp [factor₁, factor₂, ← Polynomial.map_mul, UniversalFactorizationRing.factor₁_mul_factor₂,
    Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

Premises used: Polynomial.map_mul, Polynomial.UniversalCoprimeFactorizationRing.factor₁, Polynomial.UniversalCoprimeFactorizationRing.factor₂, IsScalarTower.algebraMap_eq, Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂, Polynomial.map_map
-- 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} 𝓡' → IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
inr : Nontrivial.{u_1} 𝓡' → IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(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} 𝓡'
inl : IsCoprime 1 (↑(factor₂ m k hn p) : 𝓡'[X])
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])

Tactic:
rw [Subsingleton.elim (Subtype.val _) 1]

Premises used: Subsingleton.elim, OfNat.ofNat, Subtype.val
-- 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} 𝓡'
⊢ IsCoprime 1 (↑(factor₂ m k hn p) : 𝓡'[X])

Tactic:
isCoprime_one_left

Premises used: isCoprime_one_left
-- 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} 𝓡'
⊢ IsCoprime 1 (↑(factor₂ m k hn p) : 𝓡'[X])

Tactic:
exact isCoprime_one_left

Premises used: isCoprime_one_left
-- 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 :
  IsUnit (M := 𝓡')
    ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
        ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
          (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])) :
      𝓡')
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])

Tactic:
rw [← Polynomial.isUnit_resultant_iff_isCoprime (factor₁ m k hn p).monic, factor₁,
    factor₂, MonicDegreeEq.map_coe, MonicDegreeEq.map_coe, Polynomial.resultant_map_map,
    (UniversalFactorizationRing.factor₁ m k hn p).monic.natDegree_map,
    (UniversalFactorizationRing.factor₂ m k hn p).monic.natDegree_map]

Premises used: Polynomial.MonicDegreeEq.monic, Polynomial.UniversalFactorizationRing.factor₂, Polynomial.UniversalFactorizationRing.factor₁, Polynomial.UniversalCoprimeFactorizationRing.factor₁, Polynomial.isUnit_resultant_iff_isCoprime, Polynomial.MonicDegreeEq.map_coe, Polynomial.Monic.natDegree_map, Polynomial.resultant_map_map, Polynomial.UniversalCoprimeFactorizationRing.factor₂
-- 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} 𝓡'
⊢ IsUnit (M := 𝓡')
    ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
        ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
          (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])) :
      𝓡')

Tactic:
((IsUnit.mul_iff (x := algebraMap 𝓡 𝓡' ((-1) ^ n))).mp ?_).2

Premises used: IsUnit.mul_iff, And.right, Iff.mp
-- 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 :
  IsUnit
    (HMul.hMul (α := 𝓡') (β := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (HPow.hPow (α := 𝓡) (-1) n) : 𝓡')
      ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
          ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
            (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])) :
        𝓡'))
⊢ IsUnit (M := 𝓡')
    ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
        ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
          (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])) :
      𝓡')

Tactic:
refine ((IsUnit.mul_iff (x := algebraMap 𝓡 𝓡' ((-1) ^ n))).mp ?_).2
-- 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 : IsUnit (M := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)
⊢ IsUnit
    (HMul.hMul (α := 𝓡') (β := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (HPow.hPow (α := 𝓡) (-1) n) : 𝓡')
      ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
          ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
            (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])) :
        𝓡'))

Tactic:
rw [← map_mul, ← UniversalFactorizationRing.jacobian_resentation m k hn p]

Premises used: Polynomial.UniversalFactorizationRing.jacobian_resentation, map_mul
-- 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} 𝓡'
⊢ IsUnit (M := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)

Tactic:
IsLocalization.Away.algebraMap_isUnit _

Premises used: IsLocalization.Away.algebraMap_isUnit
-- 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} 𝓡'
⊢ IsUnit (M := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)

Tactic:
exact IsLocalization.Away.algebraMap_isUnit _

Premises used: IsLocalization.Away.algebraMap_isUnit
-- 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
Δ : 𝓡 := (presentation m k hn p).jacobian
⊢ IsUnit (M := Localization.Away Δ) ((algebraMap 𝓡 (Localization.Away Δ) : (a : 𝓡) → Localization.Away Δ) Δ)

Tactic:
have hΔ : IsUnit (algebraMap 𝓡 (Localization.Away Δ) Δ) :=
    IsLocalization.Away.algebraMap_isUnit _
-- 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
Δ : 𝓡 := (presentation m k hn p).jacobian
hΔ : IsUnit (M := Localization.Away Δ) ((algebraMap 𝓡 (Localization.Away Δ) : (a : 𝓡) → Localization.Away Δ) Δ)
⊢ IsUnit (M := Localization.Away Δ)
    (Algebra.PreSubmersivePresentation.jacobian
      (Algebra.PreSubmersivePresentation.comp
        (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ) (presentation m k hn p)))

Tactic:
simpa [Algebra.smul_def, -isUnit_map_iff, hΔ]

Premises used: isUnit_map_iff, Algebra.smul_def
-- 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
Δ : 𝓡 := (presentation m k hn p).jacobian
hΔ : IsUnit (M := Localization.Away Δ) ((algebraMap 𝓡 (Localization.Away Δ) : (a : 𝓡) → Localization.Away Δ) Δ)
P : Algebra.SubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
  let __PreSubmersivePresentation :
    Algebra.PreSubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
    Algebra.PreSubmersivePresentation.comp (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ)
      (presentation m k hn p);
  { toPreSubmersivePresentation := __PreSubmersivePresentation, jacobian_isUnit := ⋯ }
simp :
  Algebra.Presentation.dimension (S := Localization.Away Δ)
        (Algebra.PreSubmersivePresentation.toPresentation
          (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ)) +
      (presentation m k hn p).dimension =
    0
⊢ P.dimension = 0

Tactic:
simp only [Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, P]

Premises used: Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension
-- 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
Δ : 𝓡 := (presentation m k hn p).jacobian
hΔ : IsUnit (M := Localization.Away Δ) ((algebraMap 𝓡 (Localization.Away Δ) : (a : 𝓡) → Localization.Away Δ) Δ)
P : Algebra.SubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
  let __PreSubmersivePresentation :
    Algebra.PreSubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
    Algebra.PreSubmersivePresentation.comp (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ)
      (presentation m k hn p);
  { toPreSubmersivePresentation := __PreSubmersivePresentation, jacobian_isUnit := ⋯ }
⊢ Algebra.Presentation.dimension (S := Localization.Away Δ)
        (Algebra.PreSubmersivePresentation.toPresentation
          (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ)) +
      (presentation m k hn p).dimension =
    0

Tactic:
simp [Algebra.Presentation.dimension, hn]

Premises used: Algebra.Presentation.dimension