awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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])
⊢ IsCoprime (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X])
    (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X])
have h₁ : (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]) =
  (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
Tactic: convert! (isCoprime_factor₁_factor₂ m k hn p).map (Polynomial.mapRingHom f.toRingHom)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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 𝓡 𝓡'))
⊢ (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₁ m k hn p) : 𝓡'[X])
have 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]))
Tactic: simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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 𝓡 𝓡'))
⊢ (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]) =
    (mapRingHom f.toRingHom : (a : 𝓡'[X]) → S[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
have 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]))
Tactic: simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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) ⋯)
⊢ 𝓡' →ₐ[R] S
have refine : ∀ (y : ↥(Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)),
  IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (↑y : 𝓡) : S)
Tactic: refine IsLocalization.liftAlgHom (f := f)
      (M := .powers (UniversalFactorizationRing.presentation m k hn p).jacobian) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
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) ⋯)
⊢ ∀ (y : ↥(Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)),
    IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (↑y : 𝓡) : S)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ ∀ (y : ↥(Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)),
    IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (↑y : 𝓡) : S)
have 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)
Tactic: rw [Subtype.forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ ∀ (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)
have change : LE.le (α := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
  (Submonoid.comap f (IsUnit.submonoid S))
Tactic: change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ LE.le (α := Submonoid 𝓡) (Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian)
    (Submonoid.comap f (IsUnit.submonoid S))
have simp : IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (UniversalFactorizationRing.presentation m k hn p).jacobian : S)
Tactic: simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ IsUnit.{u_2} (M := S) ((f : (a : 𝓡) → S) (UniversalFactorizationRing.presentation m k hn p).jacobian : S)
have 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)
Tactic: rw [← AlgHom.coe_toRingHom, UniversalFactorizationRing.jacobian_resentation, map_mul,
      ← Polynomial.resultant_map_map, IsUnit.mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) n) : S)
have 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)
        sorry);
  IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (β := ℕ) (-1) 0) : S)
Tactic: cases n
Cleared hypotheses: n, hn, p, q, f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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)
⊢ IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) n) : S)
have 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)
        sorry);
  IsUnit.{u_2} (M := S) (((↑f : 𝓡 →+* S) : (a : 𝓡) → S) (HPow.hPow (α := 𝓡) (-1) (n + 1)) : S)
Tactic: cases n
Cleared hypotheses: n, hn, p, q, f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ 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)
have 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)
Tactic: refine ⟨by cases n <;> simp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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
⊢ 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)
have rw : IsCoprime (R := S[X]) (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
  (map (↑f : 𝓡 →+* S) (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
Tactic: rw [← (UniversalFactorizationRing.factor₁ m k hn p).monic.natDegree_map f.toRingHom,
      ← (UniversalFactorizationRing.factor₂ m k hn p).monic.natDegree_map f.toRingHom,
      AlgHom.toRingHom_eq_coe, Polynomial.isUnit_resultant_iff_isCoprime
        ((UniversalFactorizationRing.factor₁ m k hn p).monic.map _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq 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]) }
⊢ Eq (α := 𝓡 →ₐ[R] S)
    (AlgHom.comp (B := 𝓡')
      (IsLocalization.liftAlgHom (R := 𝓡) (M :=
        Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
        (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) ⋯))
        ⋯)
      (IsScalarTower.toAlgHom R 𝓡 𝓡'))
    ((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)
        ⋯))
have h : ∀ (x : 𝓡),
  Eq.{u_2 + 1} (α := S)
    ((AlgHom.comp (B := 𝓡')
            (IsLocalization.liftAlgHom (R := 𝓡) (M :=
              Submonoid.powers (UniversalFactorizationRing.presentation m k hn p).jacobian) (f :=
              (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) sorry))
              sorry)
            (IsScalarTower.toAlgHom R 𝓡 𝓡') :
          (a : 𝓡) → S)
        x :
      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) sorry) :
            𝓡 →ₐ[R] S) :
          (a : 𝓡) → S)
        x :
      S)
Tactic: ext