awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ (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) =
    f
have this₁ : IsScalarTower (MvPolynomial (Fin n) R) R S
Tactic: haveI : IsScalarTower (MvPolynomial (Fin n) R) R S := .of_algebraMap_eq' rfl
-- 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
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
⊢ (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) =
    f
have this₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
have 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])
Tactic: cases subsingleton_or_nontrivial 𝓡
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
have 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])
Tactic: cases subsingleton_or_nontrivial 𝓡
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : 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])
have 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])
Tactic: cases subsingleton_or_nontrivial ((MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
have 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])
Tactic: cases subsingleton_or_nontrivial ((MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
have 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])
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
⊢ (presentation m k hn p).jacobian =
    HPow.hPow (α := 𝓡) (-1) n * (↑(factor₁ m k hn p) : 𝓡[X]).resultant (↑(factor₂ m k hn p) : 𝓡[X])
have 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])
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
have 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])
Tactic: refine (Algebra.PreSubmersivePresentation.baseChange_jacobian _ _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ 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])
have 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])
Tactic: change fromTensor _ _ _ _ _ = _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ (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])
have 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])
Tactic: rw [MvPolynomial.universalFactorizationMapPresentation_jacobian]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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))
⊢ (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])
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
have inl : Subsingleton.{u_1 + 1} 𝓡' → IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
Tactic: cases subsingleton_or_nontrivial 𝓡'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
have inr : Nontrivial.{u_1} 𝓡' → IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
Tactic: cases subsingleton_or_nontrivial 𝓡'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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 (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
have inl : IsCoprime 1 (↑(factor₂ m k hn p) : 𝓡'[X])
Tactic: rw [Subsingleton.elim (Subtype.val _) 1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : Nontrivial.{u_1} 𝓡'
⊢ IsCoprime (↑(factor₁ m k hn p) : 𝓡'[X]) (↑(factor₂ m k hn p) : 𝓡'[X])
have inr : IsUnit (M := 𝓡')
  ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡')
      ((↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]).resultant
        (↑(UniversalFactorizationRing.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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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])) :
      𝓡')
have 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])) :
      𝓡'))
Tactic: refine ((IsUnit.mul_iff (x := algebraMap 𝓡 𝓡' ((-1) ^ n))).mp ?_).2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h : Nontrivial.{u_1} 𝓡'
⊢ 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])) :
        𝓡'))
have inr : IsUnit (M := 𝓡') ((algebraMap 𝓡 𝓡' : (a : 𝓡) → 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)
Tactic: rw [← map_mul, ← UniversalFactorizationRing.jacobian_resentation m k hn p]
-- 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
Δ : 𝓡 := (presentation m k hn p).jacobian
⊢ Algebra.Etale R 𝓡'
have hΔ : IsUnit (M := Localization.Away Δ) ((algebraMap 𝓡 (Localization.Away Δ) : (a : 𝓡) → Localization.Away Δ) Δ)
Tactic: have hΔ : IsUnit (algebraMap 𝓡 (Localization.Away Δ) Δ) :=
    IsLocalization.Away.algebraMap_isUnit _
-- 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
Δ : 𝓡 := (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 := ⋯ }
⊢ P.dimension = 0
have simp : Algebra.Presentation.dimension (S := Localization.Away Δ)
      (Algebra.PreSubmersivePresentation.toPresentation
        (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ)) +
    (presentation m k hn p).dimension =
  0
Tactic: simp only [Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, P]
-- 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
Δ : 𝓡 := (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.Etale R 𝓡'
have this : 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]⟩
-- 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 𝓡 𝓡'))
⊢ 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).1 : 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)