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

Goal state before:
pp: case inr.inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
hi : i ≤ p.natDegree
⊢ IsIntegral R (p.coeff i)

pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
hi : p.natDegree < i
⊢ IsIntegral R (p.coeff i)

Tactic:
· simpa [show i ≠ m by lia] using this

Goal state after:
case inr.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
hi : p.natDegree < i
⊢ IsIntegral R (p.coeff i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian (Hom.fiber f x)
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)

Tactic:
let g : (X.affineCover.f i ≫ f).fiber x ⟶ f.fiber x :=
      pullback.map _ _ _ _ (X.affineCover.f i) (𝟙 _) (𝟙 _) (by simp) (by simp)

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian (Hom.fiber f x)
g : Hom.fiber (X.affineCover.f i ≫ f) x ⟶ Hom.fiber f x :=
  pullback.map (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField x) f ((Spec R).fromSpecResidueField x)
    (X.affineCover.f i) (𝟙 (Spec ((Spec R).residueField x))) (𝟙 (Spec R)) ⋯ ⋯
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) x)
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
⊢ ∀ (a b c : X.AffineZariskiSite),
    (∃ f, X.basicOpen f = a.toOpens) → (∃ f, X.basicOpen f = b.toOpens) → ∃ f, X.basicOpen f = a.toOpens

Tactic:
rintro ⟨U, hU⟩ ⟨V, hV⟩ ⟨W, hW⟩ ⟨f, rfl⟩ ⟨g, rfl⟩

Goal state after:
X : Scheme
W : X.Opens
hW : IsAffineOpen W
g : ↑Γ(X, toOpens ⟨W, hW⟩)
hV : IsAffineOpen (X.basicOpen g)
f : ↑Γ(X, toOpens ⟨X.basicOpen g, hV⟩)
hU : IsAffineOpen (X.basicOpen f)
⊢ ∃ f_1, X.basicOpen f_1 = toOpens ⟨X.basicOpen f, hU⟩
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ { toFractionRing := Localization.mk (c • p) ⟨q, ⋯⟩ } = c • { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

Tactic:
← Localization.smul_mk,

Goal state after:
case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ { toFractionRing := c • Localization.mk p ⟨q, ⋯⟩ } = c • { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x✝¹ x✝ : K⟮X⟯
toFractionRing✝¹ toFractionRing✝ : FractionRing K[X]
⊢ ({ toFractionRing := toFractionRing✝¹ } + { toFractionRing := toFractionRing✝ }).toFractionRing =
    { toFractionRing := toFractionRing✝¹ }.toFractionRing + { toFractionRing := toFractionRing✝ }.toFractionRing

Tactic:
simp [← ofFractionRing_add]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk p q * Localization.mk p' q' }.liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
Localization.mk_mul,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (p * p') (q * q') }.liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ p * φ p') ⟨φ ↑q * φ ↑q', ⋯⟩ } =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ * Localization.mk (φ p') ⟨φ ↑q', hq'⟩ }

Tactic:
Localization.mk_mul,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ p * φ p') ⟨φ ↑q * φ ↑q', ⋯⟩ } =
    { toFractionRing := Localization.mk (φ p * φ p') (⟨φ ↑q, hq⟩ * ⟨φ ↑q', hq'⟩) }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (map φ hφ) { toFractionRing := 0 } = { toFractionRing := 0 }

Tactic:
← Localization.mk_zero (1 : R[X]⁰),

Goal state after:
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (map φ hφ) { toFractionRing := Localization.mk 0 1 } = { toFractionRing := 0 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ { toFractionRing := 0 }.liftOn (fun p q ↦ φ p / φ q) ⋯ = 0

Tactic:
← Localization.mk_zero (1 : R[X]⁰),

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ { toFractionRing := Localization.mk 0 1 }.liftOn (fun p q ↦ φ p / φ q) ⋯ = 0
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
hr : r ∈ integralClosure R S
hrp : r ∉ p
⊢ Function.Injective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom ⟨r, ⋯⟩)

Tactic:
by exact IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective

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✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
⊢ False

Tactic:
have hf' : Function.Injective (aeval (R := R) x) := (injective_iff_map_eq_zero _).mpr
    fun p hp ↦ not_not.mp fun hp' ↦ hx.transcendental ⟨p, hp', hp⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
hf' : Function.Injective ⇑(aeval x)
⊢ False
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✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
⊢ False

Tactic:
let := f.toRingHom.toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this : Algebra R[X] S := f.toAlgebra
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ↑↑(∏ i,
          ∏ j > i,
            if
                Fin.cast ⋯ (finSumFinEquiv (finSumFinEquiv.symm i).swap) <
                  Fin.cast ⋯ (finSumFinEquiv (finSumFinEquiv.symm j).swap) then
              1
            else -1) =
    (-1) ^ (m * n)

Tactic:
simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (∏ x,
      ∏ x_1 > x,
        if finSumFinEquiv (finSumFinEquiv.symm x).swap < finSumFinEquiv (finSumFinEquiv.symm x_1).swap then 1 else -1) =
    (-1) ^ (m * n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
mul_left_comm (f.coeff m ^ k)

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
⊢ (-1) ^ (m * (n + k)) * ((-1) ^ (m * k) * ((-1) ^ (n * m) * (f.coeff m ^ k * f.resultant g m n))) =
    f.coeff m ^ k * f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.roots = 0
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
Multiset.eq_zero_iff_forall_notMem,

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬∀ (a : K), a ∉ g.roots
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ ∃ S', (Subalgebra.toSubmodule S').FG ∧ ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)

Tactic:
refine ⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩

Goal state after:
case refine_1
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ t.Finite

case refine_2
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ ∀ x ∈ t, IsIntegral R x

case refine_3
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
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap (adjoin R t).val.toRingHom r)
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 : ℕ
g : S →ₐ[R] T
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ ((mapEquivMonic R S n) f).map ↑g =
    (mapEquivMonic R T n) (g.comp ((mapEquivMonic R S n).symm ((mapEquivMonic R S n) f)))

Tactic:
by simp [coe_mapEquivMonic_comp']

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

Tactic:
simp only [isCoprime_zero_right, isUnit_iff] at H

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
H : ∃ r, IsUnit r ∧ C r = f
⊢ ∃ n, f.resultant 0 ∣ f.leadingCoeff ^ n
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)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
⊢ (⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left γ ≫ Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}).Finite

Tactic:
dsimp [-Scheme.Hom.comp_base, γ]
      simp only [pullback.lift_fst]
      exact (Set.finite_singleton _).subset H

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

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
⊢ IsCommMonObj G

Tactic:
let G' := (Over.pullback f).obj G

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsCommMonObj G
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).FormallyUnramified
⊢ (algebraMap R T).FormallyUnramified

Tactic:
rw [formallyUnramified_algebraMap] at h' ⊢

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
⊢ Algebra.FormallyUnramified R T
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
x : P.CotangentSpace
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x

Tactic:
dsimp only [CotangentSpace] at x
  induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
exact (P.tensorCotangentSpace T).injective

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
x✝ : ↑C
⊢ (Adjunction.ofCat (adj.comp adj')).unit.app x✝ = ((Adjunction.ofCat adj).comp (Adjunction.ofCat adj')).unit.app x✝

Tactic:
simp [bicategoricalComp]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ FinitePresentation R S

Tactic:
let := f.toRingHom.toAlgebra

Goal state after:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this : Algebra R' S := f.toAlgebra
⊢ FinitePresentation R S
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum ↑T
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)

Tactic:
algebraize [f.hom, g.hom, inl.hom, inr.hom, inl.hom.comp f.hom]
  have : IsScalarTower R T P := .of_algebraMap_eq' <| congr($(h.1.1).hom)
  have : Algebra.IsPushout R S T P := CommRingCat.isPushout_iff_isPushout.mp h
  exact Algebra.rankAtStalk_eq_of_isPushout R S T P x

Goal state after: