mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 2 < 5
hj : 4 < 5
⊢ 2 + 1 = 3

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝³ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝² : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝¹ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝ : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
hφ : (CommRingCat.Hom.hom φ).Etale
this : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) :=
  (pullbackSpecIso (↑Γ(S, U)) R ↑Γ(X, V)).symm ≪≫
    pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)))
      (Spec.map (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↑Γ(X, V))))
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) :=
  e₁.hom ≫
    pullback.map (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)
      (IsAffineOpen.fromSpec hV) (𝟙 (Spec (CommRingCat.of R))) (IsAffineOpen.fromSpec hU) ⋯ ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := g ''ᵁ PrimeSpectrum.basicOpen e
⊢ IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))

Tactic:
by

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 = 3
hi : 3 < 5
hj : 0 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 3 < 5
hj : 1 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 3 < 5
hj : 2 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi hj : 3 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 3 < 5
hj : 4 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'

Tactic:
by

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 = 3
hi : 4 < 5
hj : 0 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 4 < 5
hj : 1 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 4 < 5
hj : 2 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi : 4 < 5
hj : 3 < 5
⊢ 2 + 1 = 3

Tactic:
by

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 = 3
hi hj : 4 < 5
⊢ 2 + 1 = 3

Tactic:
by

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
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
⊢ q.Monic

Tactic:
by

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
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m' + 1) * q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) :=
  (pullbackSpecIso (↑Γ(S, U)) R ↑Γ(X, V)).symm ≪≫
    pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)))
      (Spec.map (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↑Γ(X, V))))
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) :=
  e₁.hom ≫
    pullback.map (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)
      (IsAffineOpen.fromSpec hV) (𝟙 (Spec (CommRingCat.of R))) (IsAffineOpen.fromSpec hU) ⋯ ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := g ''ᵁ PrimeSpectrum.basicOpen e
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
⊢ IsOpen (↑W₁)ᶜ

Tactic:
by

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
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ (aeval s) f = 0

Tactic:
by

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'
⊢ ∃ 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:
by

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 = 3
⊢ (Matrix.reindex (finCongr ⋯) (finCongr ⋯)) f.sylvesterDeriv =
    !![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
      f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
      f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
      f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
      0, 1, 0, 0, 3]

Tactic:
by

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 = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ !![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
          f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
          f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
          f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
          0, 1, 0, 0, 3].det *
      (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Tactic:
simp [Matrix.det_succ_row_zero (n := 4), Matrix.det_succ_row_zero (n := 3), Fin.succAbove,
    Matrix.det_fin_three, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, hf]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ (f.coeff 0 *
          (f.coeff 0 * (3 * f.coeff 3 * (3 * f.coeff 3) * 3) +
              -(2 * f.coeff 2 *
                  (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                    f.coeff 1 * (3 * f.coeff 3))) +
            f.coeff 1 * (-(3 * f.coeff 3 * f.coeff 2 * 3) + 3 * f.coeff 3 * (2 * f.coeff 2))) +
        f.coeff 1 *
          (f.coeff 1 *
                (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                  f.coeff 1 * (3 * f.coeff 3)) +
              -(f.coeff 0 * (f.coeff 2 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 3 * 3)) +
            f.coeff 1 *
              (f.coeff 2 * f.coeff 2 * 3 - f.coeff 2 * (2 * f.coeff 2) - f.coeff 1 * f.coeff 3 * 3 +
                f.coeff 1 * f.coeff 3))) *
      (-1) ^ 3 =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
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'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
⊢ (aeval s₀) f = 0

Tactic:
by

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.degree = 3
⊢ f.discr =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
⊢ IsIso (normalizationPullback f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (𝟙 X) (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) ≫ μ = toUnit X ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
f : X ⟶ G
⊢ lift (f ≫ ι) f ≫ μ = (f ≫ lift ι (𝟙 G)) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
f : X ⟶ G
⊢ (f ≫ lift ι (𝟙 G)) ≫ μ = toUnit X ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G✝ H✝ X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G✝
inst✝ : GrpObj H✝
G H : Grp C
α : yonedaGrp.obj G ⟶ yonedaGrp.obj H
⊢ yonedaGrp.map (Grp.homMk' (yonedaMonFullyFaithful.preimage (Functor.whiskerRight α (forget₂ GrpCat MonCat)))) = α

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝¹ : Field K
X : Scheme
G : Over (Spec (CommRingCat.of K))
inst✝ : GrpObj G
⊢ Over.Hom.left η ≫ G.hom = 𝟙 (Spec (CommRingCat.of K))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this : Nonempty ↥G.left
⊢ IsProper (G ⊗ G).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝² : Nonempty ↥G.left
this✝¹ : IsProper (G ⊗ G).hom
this✝ : JacobsonSpace ↥(G ⊗ G).left
this : Surjective G.hom
⊢ IsProper (Over.Hom.left (fst G G))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝³ : Nonempty ↥G.left
this✝² : IsProper (G ⊗ G).hom
this✝¹ : JacobsonSpace ↥(G ⊗ G).left
this✝ : Surjective G.hom
this : IsProper (Over.Hom.left (fst G G))
⊢ Surjective (Over.Hom.left (fst G G))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
X✝ Y✝ : Grp C
f : X✝ ⟶ Y✝
⊢ Grp.homMk' (yonedaMonFullyFaithful.preimage (Functor.whiskerRight (yonedaGrp.map f) (forget₂ GrpCat MonCat))) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
⊢ yonedaGrp.essImage = fun F ↦ (F ⋙ forget GrpCat).IsRepresentable

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
G H X : C
inst✝² : GrpObj G
inst✝¹ : GrpObj H
f : X ⟶ G
g : G ⟶ H
inst✝ : IsMonHom g
⊢ f⁻¹ ≫ g = (f ≫ g)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G X Y : C
inst✝ : GrpObj G
f : X ⟶ Y
g : Y ⟶ G
n : ℕ
⊢ f ≫ g ^ ↑n = (f ≫ g) ^ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G X Y : C
inst✝ : GrpObj G
f : X ⟶ Y
g : Y ⟶ G
n : ℕ
⊢ f ≫ g ^ Int.negSucc n = (f ≫ g) ^ Int.negSucc n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁴ : Nonempty ↥G.left
this✝³ : IsProper (G ⊗ G).hom
this✝² : JacobsonSpace ↥(G ⊗ G).left
this✝¹ : Surjective G.hom
this✝ : IsProper (Over.Hom.left (fst G G))
this : Surjective (Over.Hom.left (fst G G))
⊢ IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ ι = (𝟙 G)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ η ≫ ι = η

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁵ : Nonempty ↥G.left
this✝⁴ : IsProper (G ⊗ G).hom
this✝³ : JacobsonSpace ↥(G ⊗ G).left
this✝² : Surjective G.hom
this✝¹ : IsProper (Over.Hom.left (fst G G))
this✝ : Surjective (Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
⊢ IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
X G : C
f : X ⟶ G
inst✝ : GrpObj G
⊢ F.map f⁻¹ = (F.map f)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X G : C
inst✝ : GrpObj G
f₁ f₂ : X ⟶ G
⊢ lift f₁ f₂ ≫ conj G = f₁ * f₂ * f₁⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X G : C
inst✝ : GrpObj G
f₁ f₂ : X ⟶ G
⊢ lift f₁ f₂ ≫ commutator G = f₁ * f₂ * f₁⁻¹ * f₂⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ η ▷ G ≫ commutator G = toUnit (𝟙_ C ⊗ G) ≫ η

Tactic:
by

Goal state after: