awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.IsStandardSmoothOfRelativeDimension 0 R (Localization.Away Δ)

Tactic:
have : Algebra.IsStandardSmoothOfRelativeDimension 0 R (Localization.Away Δ) :=
    ⟨_, _, _, inferInstance, P, by
      simp only [Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, P]
      simp [Algebra.Presentation.dimension, hn]⟩
-- 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 := ⋯ }
this : Algebra.IsStandardSmoothOfRelativeDimension 0 R (Localization.Away Δ)
⊢ Algebra.Etale R 𝓡'

Tactic:
infer_instance
-- 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
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
⊢ IsCoprime.{u_2} (R := S[X]) ((mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₁ m k hn p) : 𝓡'[X]) : S[X])
    ((mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₂ m k hn p) : 𝓡'[X]) : S[X])

Tactic:
(isCoprime_factor₁_factor₂ m k hn p).map (Polynomial.mapRingHom f.toRingHom)

Premises used: IsCoprime.map, AlgHom.toRingHom, Polynomial.mapRingHom, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂
-- 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
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
h :
  (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₁ m k hn p) : 𝓡'[X])
h₁ :
  (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
⊢ IsCoprime (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X])
    (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X])

Tactic:
convert! (isCoprime_factor₁_factor₂ m k hn p).map (Polynomial.mapRingHom f.toRingHom)

Premises used: IsCoprime.map, AlgHom.toRingHom, Polynomial.mapRingHom, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂
-- 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
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
h :
  Eq (α := S[X]) (map (↑f : 𝓡' →+* S) (map (algebraMap 𝓡 𝓡') (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X])))
    (map (↑f : 𝓡' →+* S) (↑(factor₁ m k hn p) : 𝓡'[X]))
⊢ (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₁ m k hn p) : 𝓡'[X])

Tactic:
simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]

Premises used: AlgHom.comp_toRingHom, Polynomial.UniversalFactorizationRing.homEquiv, 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
f : 𝓡' →ₐ[R] S
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
h :
  Eq (α := S[X]) (map (↑f : 𝓡' →+* S) (map (algebraMap 𝓡 𝓡') (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])))
    (map (↑f : 𝓡' →+* S) (↑(factor₂ m k hn p) : 𝓡'[X]))
⊢ (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₂ m k hn p) : 𝓡'[X])

Tactic:
simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]

Premises used: AlgHom.comp_toRingHom, Polynomial.UniversalFactorizationRing.homEquiv, 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
f : 𝓡' →ₐ[R] S
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
⊢ Eq (α := S[X]) (map (↑f : 𝓡' →+* S) (map (algebraMap 𝓡 𝓡') (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X])))
    (map (↑f : 𝓡' →+* S) (↑(factor₁ m k hn p) : 𝓡'[X]))

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
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) } :=
  (UniversalFactorizationRing.homEquiv S m k hn p :
      (a : 𝓡 →ₐ[R] S) →
        { q : MonicDegreeEq S m × MonicDegreeEq S k //
          (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) })
    (f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
⊢ Eq (α := S[X]) (map (↑f : 𝓡' →+* S) (map (algebraMap 𝓡 𝓡') (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X])))
    (map (↑f : 𝓡' →+* S) (↑(factor₂ m k hn p) : 𝓡'[X]))

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
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
refine :
  ∀ (y : ↥(Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)),
    IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (↑y : 𝓡) : S)
⊢ 𝓡' →ₐ[R] S

Tactic:
refine IsLocalization.liftAlgHom (f := f)
      (M := .powers (UniversalFactorizationRing.presentation m k hn p).jacobian) ?_

Premises used: IsLocalization.liftAlgHom
-- 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
⊢ Nontrivial S

Tactic:
nontriviality S
-- 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
rw :
  ∀ (a : 𝓡)
    (b :
      Membership.mem (γ := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
        a),
    IsUnit.{u_2} (M := S)
      ((f : (a : 𝓡) → S)
          (↑(Subtype.mk (p := fun (a : 𝓡) ↦
                Membership.mem (γ := Submonoid 𝓡)
                  (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) a)
                a b) :
            𝓡) :
        S)
⊢ ∀ (y : ↥(Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)),
    IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (↑y : 𝓡) : S)

Tactic:
rw [Subtype.forall]

Premises used: Subtype.forall
-- 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
change :
  LE.le (α := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
    (Submonoid.comap f (IsUnit.submonoid S))
⊢ ∀ (a : 𝓡)
    (b :
      Membership.mem (γ := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
        a),
    IsUnit.{u_2} (M := S)
      ((f : (a : 𝓡) → S)
          (↑(Subtype.mk (p := fun (a : 𝓡) ↦
                Membership.mem (γ := Submonoid 𝓡)
                  (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) a)
                a b) :
            𝓡) :
        S)

Tactic:
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap f

Premises used: IsUnit.submonoid, Submonoid.comap, Submonoid.powers
-- 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
simp : IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (UniversalFactorizationRing.presentation m k hn p).jacobian : S)
⊢ LE.le (α := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
    (Submonoid.comap f (IsUnit.submonoid S))

Tactic:
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]

Premises used: Submonoid.mem_comap, IsUnit.mem_submonoid_iff, Submonoid.powers_le
-- 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
rw :
  IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) n) : S) ∧
    IsUnit
      (resultant (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
        (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
        (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).natDegree
        (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]).natDegree)
⊢ IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (UniversalFactorizationRing.presentation m k hn p).jacobian : S)

Tactic:
rw [← AlgHom.coe_toRingHom, UniversalFactorizationRing.jacobian_resentation, map_mul,
      ← Polynomial.resultant_map_map, IsUnit.mul_iff]

Premises used: IsUnit.mul_iff, AlgHom.coe_toRingHom, Polynomial.UniversalFactorizationRing.jacobian_resentation, map_mul, Polynomial.resultant_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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
zero :
  ∀ (hn : 0 = m + k) (p : MonicDegreeEq R 0)
    (q :
      { q : MonicDegreeEq S m × MonicDegreeEq S k //
        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }),
    let f : 𝓡 →ₐ[R] S :=
      (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
          (a :
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
            𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k)
          ⋯);
    IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (β := ℕ) (-1) 0) : S)
succ :
  ∀ (n : ℕ) (hn : n + 1 = m + k) (p : MonicDegreeEq R (n + 1))
    (q :
      { q : MonicDegreeEq S m × MonicDegreeEq S k //
        (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }),
    let f : 𝓡 →ₐ[R] S :=
      (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
          (a :
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
            𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k)
          ⋯);
    IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) (n + 1)) : S)
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) n) : S)

Tactic:
cases n
-- 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
m k : ℕ
h : Nontrivial S
hn : 0 = m + k
p : MonicDegreeEq R 0
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (β := ℕ) (-1) 0) : S)

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
m k : ℕ
h : Nontrivial S
n : ℕ
hn : n + 1 = m + k
p : MonicDegreeEq R (n + 1)
q :
  { q : MonicDegreeEq S m × MonicDegreeEq S k //
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) (n + 1)) : S)

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 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]) ∧ IsCoprime (↑q.1 : S[X]) (↑q.2 : S[X]) }
f : 𝓡 →ₐ[R] S :=
  (Equiv.symm (UniversalFactorizationRing.homEquiv S m k hn p) :
      (a :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) →
        𝓡 →ₐ[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])) (↑q : MonicDegreeEq S m × MonicDegreeEq S k) ⋯)
h : Nontrivial S
refine :
  IsUnit
    (resultant (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
      (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
      (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).natDegree
      (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]).natDegree)
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) n) : S) ∧
    IsUnit
      (resultant (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
        (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
        (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).natDegree
        (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]).natDegree)

Tactic:
refine ⟨by cases n <;> simp, ?_⟩