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

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ ↑s
⊢ r ^ s.sup m * x ∈ ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})

Tactic:
simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ app (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) U ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯).op =
    (CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
        (normalizationObjIso f hU).inv) ≫
      app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)

Tactic:
← cancel_mono (((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ (app (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) U ≫
        ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯).op) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op =
    ((CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
          (normalizationObjIso f hU).inv) ≫
        app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    appLE (toNormalization f) (fromNormalization f ⁻¹ᵁ U) (f ⁻¹ᵁ U) ⋯

Tactic:
by
  rw [appLE, f.toNormalization_app_preimage ⟨U, hU⟩, Category.assoc]
  simp [← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
x : S
hx : x ∈ ↑s
⊢ (fun x ↦ r ^ x) (s.sup m) * x ∈ ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})

Tactic:
simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]

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
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H : ZariskisMainProperty R p
⊢ QuasiFiniteAt R p

Tactic:
obtain ⟨S', hS', r, hrp, H⟩ := H.exists_fg_and_exists_notMem_and_awayMap_bijective _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
⊢ QuasiFiniteAt R p
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
⊢ (Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯).comp
      (universalFactorizationMap R n m k hn) =
    (mapEquivMonic R S n).symm p

Tactic:
by
    refine (mapEquivMonic R S n).eq_symm_apply.mpr <| Subtype.ext ?_
    simp only [universalFactorizationMap, coe_mapEquivMonic_comp, Equiv.apply_symm_apply,
      Polynomial.map_mul]
    simp [← coe_mapEquivMonic_comp, ← q.2]

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

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ φ (f'.resultant g₁' * f'.resultant g₂') = φ (f'.resultant g₁') * φ (f'.resultant g₂')

Tactic:
map_mul

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

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
b : R[X]
e : 0 * f + b * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right b (by simpa using e))

Goal state after:
case inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
b : R[X]
r : R
hr : IsUnit r
H : IsCoprime f (C r)
hg : C r ≠ 0
e : 0 * f + b * C r = 1
⊢ ∃ n, f.resultant (C r) ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k))
        (freeMonic R m).natDegree (freeMonic R k).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
MonicDegreeEq.natDegree,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k))
        (freeMonic R m).natDegree (freeMonic R k).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k))
        (freeMonic R m).natDegree (freeMonic R k).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m

Tactic:
MonicDegreeEq.natDegree,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k))
        (freeMonic R m).natDegree (freeMonic R k).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m k
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
Δ : 𝓡 := (presentation m k hn p).jacobian
hΔ : IsUnit ((algebraMap 𝓡 (Localization.Away Δ)) Δ)
P : Algebra.SubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
  let __PreSubmersivePresentation :=
    (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ).comp (presentation m k hn p);
  { toPreSubmersivePresentation := __PreSubmersivePresentation, jacobian_isUnit := ⋯ }
⊢ P.dimension = 0

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : (Matrix.reindex e e) f.sylvesterDeriv = !![1]
⊢ f.discr = 1

Tactic:
simp [discr, ← Matrix.det_reindex_self e, this, hf]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
⊢ False

Tactic:
have : q's.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint (.powers s₂) _ _ ‹_› hq's

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this✝ : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
this : q's.IsPrime
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
      else if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨0, hi⟩

Tactic:
· simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
    fin_cases hj' <;> 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»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
      else if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨1, hi⟩

Tactic:
· simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
    fin_cases hj' <;> 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»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨2, hi⟩

Tactic:
· simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
    fin_cases hj' <;> 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»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨3, hi⟩

Tactic:
· simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
    fin_cases hj' <;> 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 «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * (↑(4 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨4, hi⟩

Tactic:
· simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
    fin_cases hj' <;> simp [mul_comm, one_add_one_eq_two, (by norm_num : (2 : R) + 1 = 3)]

Goal state after: