mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx✝ : IsIntegral S a
𝓟 : StandardEtalePresentation R S
n : ℕ
hx : ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
⊢ a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))

Tactic:
obtain ⟨a, rfl⟩ := (Algebra.TensorProduct.comm _ _ _).surjective a

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : B ⊗[R] S
hx✝ : IsIntegral S ((Algebra.TensorProduct.comm R B S) a)
hx : ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • (Algebra.TensorProduct.comm R B S) a)
⊢ (Algebra.TensorProduct.comm R B S) a ∈
    Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e✝ : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e✝.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e✝.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
x✝ : R
⊢ (((AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B))).comp C) x✝ = ((e.comp (AdjoinRoot.mk 𝓟.f)).comp C) x✝

Tactic:
simp [e]

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case h₂
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := ⋯
e✝ : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := ⋯
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e✝.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e✝.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f := ⋯
⊢ ((AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B))) X = (e.comp (AdjoinRoot.mk 𝓟.f)) X

Tactic:
simp [e]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ φ p * t - p.leadingCoeff • t * φ X ^ p.natDegree ∈ (conductor R (φ X)).radical

Tactic:
exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
replace hg : g ∉ p := by simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
⊢ f.sylvester g m n =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m)

Tactic:
ext i j
  induction j using Fin.addCases <;> simp [sylvester]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ ((pullbackRestrictIsoRestrict f ↑U).inv ≫
        Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          (pullbackRestrictIsoRestrict f ↑V).hom) ≫
      (f ⁻¹ᵁ ↑V).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ ↑V).ι
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑(Fin.castAdd n j₂) + 1 ≤ m
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.castAdd n j₂) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)

Tactic:
| left j₂ =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = r ^ ↑(Fin.castAdd n j₂) * M₂.det
hi : ↑(Fin.castAdd n j₂) + 1 ≤ m
⊢ r *
      Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then r * g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)

Tactic:
| left j₂ =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ (C g.leadingCoeff⁻¹ * g).Monic

Tactic:
rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ g.leadingCoeff⁻¹ * g.coeff g.natDegree = 1
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ (universalFactorizationMapPresentation R n m k hn).jacobiMatrix =
    -((Matrix.reindex (finCongr ⋯) (finCongr ⋯))
          ((Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)).toRingHom
                (freeMonic R m)).sylvester
            (Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)).toRingHom
              (freeMonic R k))
            m k)).transpose

Tactic:
let := (universalFactorizationMap R n m k hn).toAlgebra

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (universalFactorizationMapPresentation R n m k hn).jacobiMatrix =
    -((Matrix.reindex (finCongr ⋯) (finCongr ⋯))
          ((Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)).toRingHom
                (freeMonic R m)).sylvester
            (Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)).toRingHom
              (freeMonic R k))
            m k)).transpose
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
⊢ (universalFactorizationMapPresentation R n m k hn).jacobian =
    (-1) ^ n *
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
        (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))

Tactic:
let := (universalFactorizationMap R n m k hn).toAlgebra

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (universalFactorizationMapPresentation R n m k hn).jacobian =
    (-1) ^ n *
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
        (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ (universalFactorizationMap R n m k hn).IsIntegral

Tactic:
let := (universalFactorizationMap R n m k hn).toAlgebra

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (universalFactorizationMap R n m k hn).IsIntegral
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ f.resultant f = 0 ^ f.natDegree

Tactic:
induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf =>
    by_cases h : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
    simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]
  | injective R S φ hφ f IH =>
    apply hφ
    simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((algebraMap 𝓡 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)

Tactic:
exact IsLocalization.Away.algebraMap_isUnit _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this : Q.IsPrime
⊢ P = Ideal.comap (algebraMap R 𝓡') Q

Tactic:
RingHom.comap_ker,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this : Q.IsPrime
⊢ P = RingHom.ker (φ.comp (algebraMap R 𝓡'))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 0 < 5
⊢ (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
    else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * (↑(0 - (0 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
    else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * (↑(0 - (1 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
    else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * (↑(0 - (2 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
    else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * (↑(0 - (3 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 = 0 then f.coeff (0 - 4) else 0
    else if 4 ≤ 2 then f.coeff (0 - (4 - 2) + 1) * (↑(0 - (4 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨4, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
    else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * (↑(1 - (0 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
    else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * (↑(1 - (1 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
    else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * (↑(1 - (2 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
    else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * (↑(1 - (3 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 1 then f.coeff (1 - 4) else 0
    else if 4 ≤ 3 then f.coeff (1 - (4 - 2) + 1) * (↑(1 - (4 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨4, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 2 then f.coeff (2 - 0) else 0
    else if 0 ≤ 4 then f.coeff (2 - (0 - 2) + 1) * (↑(2 - (0 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨0, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 2 then f.coeff (2 - 1) else 0
    else if 1 ≤ 4 then f.coeff (2 - (1 - 2) + 1) * (↑(2 - (1 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨1, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 2 then f.coeff (2 - 2) else 0
    else if 2 ≤ 4 then f.coeff (2 - (2 - 2) + 1) * (↑(2 - (2 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨2, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 2 then f.coeff (2 - 3) else 0
    else if 3 ≤ 4 then f.coeff (2 - (3 - 2) + 1) * (↑(2 - (3 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨3, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 2 then f.coeff (2 - 4) else 0
    else if 4 ≤ 4 then f.coeff (2 - (4 - 2) + 1) * (↑(2 - (4 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨4, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «3».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 3 then f.coeff (3 - 0) else 0
    else if 0 ≤ 5 ∧ 1 ≤ 0 - 2 then f.coeff (3 - (0 - 2) + 1) * (↑(3 - (0 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨0, hj⟩

Tactic:
simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after: