mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (if q = 0 then (0, 1)
    else
      have r := gcd p q;
      (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))) =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

pp: case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        have r := gcd p 0;
        (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        have r := gcd 0 1;
        (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
if_neg hq

Goal state after:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (have r := gcd p q;
    (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))) =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        have r := gcd p 0;
        (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        have r := gcd 0 1;
        (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePair R
⊢ Algebra.FormallyEtale R P.Ring

Tactic:
refine Algebra.FormallyEtale.iff_comp_bijective.mpr fun S _ _ I hI ↦ ?_
  rw [← P.homEquiv.symm.bijective.of_comp_iff, ← P.homEquiv.bijective.of_comp_iff']
  suffices ∀ x, P.HasMap (Ideal.Quotient.mk I x) → ∃! a : { x : S // P.HasMap x }, a - x ∈ I by
    simpa [Function.bijective_iff_existsUnique, Ideal.Quotient.mk_surjective.forall,
      Subtype.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  intro x hx
  obtain ⟨ε, ⟨hεI, hε⟩, H⟩ := P.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot I hI _ hx
  exact ⟨⟨x + ε, hε⟩, by simpa, fun y hy ↦
    Subtype.ext (sub_eq_iff_eq_add'.mp (H _ ⟨hy, by simpa using y.2⟩))⟩

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

Goal state before:
pp: case refine_4
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
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})

Tactic:
apply Ideal.Quotient.algHom_ext

Goal state after:
case refine_4
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
P : StandardEtalePair R
⊢ ((P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
              ⋯).comp
          (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
            (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯)).comp
      (Ideal.Quotient.mkₐ R (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) =
    (AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})).comp
      (Ideal.Quotient.mkₐ R (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hp : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
hw : Polynomial.map (algebraMap R P.ResidueField) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 2) +
      Polynomial.map (algebraMap R P.ResidueField) p =
    Polynomial.map (algebraMap R P.ResidueField) p *
      (1 + w * (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 1))

Tactic:
ring

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
p : Ideal S
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ (n + 1))
⊢ IsIntegral R r

Tactic:
exact (IsIntegral.pow_iff (by simp)).mp hn

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
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
⊢ φ r ≠ 0

Tactic:
have : Ideal.ResidueField.mapₐ p Q (ofId R S) (Ideal.over_def Q p) =
      AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField) := by ext

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ φ r ≠ 0
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (algebraMap S T) a = (algebraMap S T) t ^ n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ ((algebraMap S T) s ^ m) ^ k * ((algebraMap S T) s ^ 1) ^ k * (algebraMap S T) t ^ k *
        (((algebraMap S T) s ^ m) ^ n * ((algebraMap S T) s ^ 1) ^ n * (algebraMap S T) t ^ n) *
      x =
    (algebraMap S T) s ^ ((m + 1) * n) * (((algebraMap S T) s ^ m) ^ k * (algebraMap S T) t ^ k) *
      ((algebraMap S T) s ^ k * ((algebraMap S T) t ^ n * x))

Tactic:
ring

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
p : R[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝¹ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this✝ : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R'[X]
hq : IsIntegral R' ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q)
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = (fun x ↦ a ^ x) n • q
this : IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q'))
m : ℕ
hm : IsIntegral R ((algebraMap S S') ((algebraMap R S) (a ^ m) * ((algebraMap R S) (a ^ n) * t - φ q')))
k : ℕ
hk : IsIntegral R ((fun x ↦ a ^ x) k • ((algebraMap R S) (a ^ m) * ((algebraMap R S) (a ^ n) * t - φ q')))
⊢ (algebraMap R S) a ^ (k + m + n) * t - (algebraMap R S) a ^ (k + m) * φ q' =
    (algebraMap R S) a ^ k * ((algebraMap R S) a ^ m * ((algebraMap R S) a ^ n * t - φ q'))

Tactic:
ring

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
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
⊢ φ p * (t * x) = φ p * t * x

Tactic:
ring

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
(Tactic.tacticHave__
 "have"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `inst)
   []
   [(Term.typeSpec
     ":"
     (Term.app
      `Unramified
      [`R (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `Localization.Away [`s]) ")")]))]
   ":="
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))

Goal state after:
case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
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 : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {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 : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p

Tactic:
let inst : Algebra (integralClosure R S) (Localization.AtPrime p) :=
      OreLocalization.instAlgebra
    have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
    refine .restrictScalars (this p (aeval (f X)) ?_ (integralClosure_idem (R := R)))
    refine RingHom.Finite.of_comp_finite (f := mapRingHom (algebraMap R _)) ?_
    convert! (show f.toRingHom.Finite from hf)
    ext <;> simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes]

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.affineOpens
⊢ (pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι ≫ toNormalization f =
    (pullbackRestrictIsoRestrict f ↑U).hom ≫
      (f ⁻¹ᵁ ↑U).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
          (normalizationOpenCover f).f U

Tactic:
← Category.assoc

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (pullbackRestrictIsoRestrict f ↑U).hom ≫
      (f ⁻¹ᵁ ↑U).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
          (normalizationOpenCover f).f U
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
⊢ f.resultant (g + f * p) m n = f.resultant g m n

Tactic:
have H : p.support ⊆ Finset.range (n - m + 1) := by
    simp only [Finset.subset_iff, Finset.mem_range]
    exact fun x hx ↦ (le_natDegree_of_mem_supp _ hx).trans_lt (by lia)

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * p) m n = f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hk : p.natDegree + n ≤ m
hg : g.natDegree ≤ n
⊢ ((-1) ^ 2) ^ (n * m) * f.resultant g m n = f.resultant g m n

Tactic:
ring

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k✝ : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ (-1) ^ n * g.coeff n * ((-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n) =
    (-1) ^ (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n

Tactic:
ring

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
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.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
let K := FractionRing R
    apply FaithfulSMul.algebraMap_injective R K
    have := this (f.map (algebraMap R K)) (g.map (algebraMap R K)) n (natDegree_map_le.trans hg)
      (hf.map _) (Field.toIsField _)
    simp only [resultant_map_map, natDegree_map_eq_of_injective, leadingCoeff_map_of_injective,
      FaithfulSMul.algebraMap_injective R K, ← hf.natDegree_eq_card_roots,
      ← roots_map_of_injective_of_card_eq_natDegree] at this
    simpa [map_multiset_prod, aeval_algebraMap_apply, Multiset.map_map] using this

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 : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ normalizationDesc f
        ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
          coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
      coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
        (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    𝟙 (normalization f)

Tactic:
by
    refine Scheme.Hom.normalization.hom_ext _ _ _ f.fromNormalization ?_ (by simp) (by simp)
    rw [← cancel_epi (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv]
    apply coprod.hom_ext <;> simp

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

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

pp: case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
· simp only [isCoprime_zero_right, isUnit_iff] at H
    aesop

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ f.leadingCoeff ^ g.natDegree * ((r ^ g.natDegree) ^ f.natDegree * (Multiset.map (fun i ↦ eval i g) f.roots).prod) =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)

Tactic:
ring

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

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
pq : ↥R[X]_m × ↥R[X]_n
⊢ f * ↑pq.2 + g * ↑pq.1 ∈ R[X]_(m + n)

Tactic:
by
    obtain ⟨⟨p, hp⟩, ⟨q, hq⟩⟩ := pq
    rw [Polynomial.mem_degreeLT]
    refine (degree_add_le _ _).trans_lt (max_lt ?_ ?_)
    · by_cases hf' : f = 0; · simp_all
      exact (degree_mul_le _ _).trans_lt (WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hf) (by simpa using hq))
    · by_cases hg' : g = 0; · simp_all
      exact (degree_mul_le _ _).trans_lt ((WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hg) (by simpa using hp)).trans_eq (add_comm _ _))

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

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ f * (↑x✝¹.2 + ↑x✝.2) + g * (↑x✝¹.1 + ↑x✝.1) = f * ↑x✝¹.2 + g * ↑x✝¹.1 + (f * ↑x✝.2 + g * ↑x✝.1)

Tactic:
ring

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0

Tactic:
obtain ⟨q, hq, hq'⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd
      ((minpoly R s).map (algebraMap R p.ResidueField)) ((minpoly.monic hRs).map _).ne_zero 0

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    (X - C 0) ^ rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) * q
hq' : ¬X - C 0 ∣ q
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0