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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
⊢ ↑f.vars ⊆ Set.range Subtype.val

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
q : Ideal S
inst✝ : q.IsPrime
q' : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ q = q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) ⊥

Tactic:
simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ q = q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) ⊥

Tactic:
simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
⊢ (residueFieldMapCAlgEquiv I J hJ) ((residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X) =
    (residueFieldMapCAlgEquiv I J hJ) ((algebraMap R[X] J.ResidueField) X)

Tactic:
by simp

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

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
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
this : QuasiFiniteAt S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q)
H : Ideal.map (algebraMap R T) (Ideal.under R q) ≤ Ideal.map (algebraMap S T) (Ideal.under S q)
⊢ q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) ⊥ =
    q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap S T) (Ideal.under S q))) ⊥

Tactic:
simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
this : ∀ (x : ↥Y), IsLocallyArtinian (Hom.fiber f x)
⊢ (Y.affineCover.X i).fromSpecResidueField x ≫ Y.affineCover.f i =
    Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x) ≫ Y.fromSpecResidueField ((Y.affineCover.f i) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: 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)
⊢ (X.affineCover.f i ≫ f) ≫ 𝟙 (Spec R) = X.affineCover.f i ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: 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)
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) = 𝟙 (Spec ((Spec R).residueField x)) ≫ (Spec R).fromSpecResidueField x

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
r : ↑Γ(X, ↑U)
this✝ : IsLocalization.Away ((ConcreteCategory.hom (α.app (Opposite.op U))) r) ↑(F.obj (Opposite.op (U.basicOpen r)))
this : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen r))) :=
  (CommRingCat.Hom.hom (F.map (homOfLE ⋯).op)).toAlgebra
⊢ ↑(Hom.opensRange ((relativeGluingData H).functor.map (homOfLE ⋯))) =
    ↑(PrimeSpectrum.basicOpen ((ConcreteCategory.hom (α.app (Opposite.op U))) r))

Tactic:
refine PrimeSpectrum.localization_away_comap_range (F.obj (.op <| U.basicOpen r))
    (α.app (.op U) r)

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

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ✝ : K[X] →ₐ[S] L
hφ✝ : K[X]⁰ ≤ Submonoid.comap φ✝ L⁰
φ : K[X] →ₐ[S] R[X]
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
r : S
⊢ (↑↑(mapRingHom φ hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S R⟮X⟯) r

Tactic:
simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ↑((Units.map ↑f.toRingHom) ⋯.unit)⁻¹ = ↑g.toRingHom ↑⋯.unit⁻¹

Tactic:
← Units.coe_map_inv

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ↑((Units.map ↑f.toRingHom) ⋯.unit)⁻¹ = ↑((Units.map ↑g.toRingHom) ⋯.unit)⁻¹
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ (P.lift P.X ⋯) P.X = (AlgHom.id R P.Ring) P.X

Tactic:
by simp

Goal state after:
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
f : P.Ring →ₐ[R] S
⊢ ((fun x ↦ P.lift ↑x ⋯) ((fun f ↦ ⟨f P.X, ⋯⟩) f)) P.X = f P.X

Tactic:
by simp

Goal state after:
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
x : { x // P.HasMap x }
⊢ (fun f ↦ ⟨f P.X, ⋯⟩) ((fun x ↦ P.lift ↑x ⋯) x) = x

Tactic:
by simp

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

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ num 0 = 0

Tactic:
convert! num_div' (0 : K[X]) one_ne_zero

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
⊢ 0 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (0 / gcd 0 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ x.denom.Monic

Tactic:
induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

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

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ q / gcd p q ∣ q

pp: case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0

Tactic:
· exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)

Goal state after:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0
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
⊢ {C P.f, Y * C P.g - 1}.Finite

Tactic:
by simp

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
f g : S
H : HasStandardEtaleSurjectionOn R f
h : f ∣ g
⊢ HasStandardEtaleSurjectionOn R g

Tactic:
by
  obtain ⟨P, φ, hsurj⟩ := H
  obtain ⟨g, rfl⟩ := h
  obtain ⟨a, ha⟩ := hsurj (algebraMap _ _ g)
  have : IsLocalization.Away (f * g) (Localization.Away (φ a)) :=
    ha ▸ .mul' (Localization.Away f) _ _ _
  have : IsStandardEtale R (Localization.Away a) := .of_isLocalizationAway a
  exact .mk _ (IsLocalization.Away.mapₐ_surjective_of_surjective
    (Aₚ := Localization.Away a) (Bₚ := Localization.Away (φ a)) a hsurj)

Goal state after:
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
P : StandardEtalePresentation R S
e : S ≃ₐ[R] T
⊢ (P.lift (e P.x) ⋯) P.X = ((↑e).comp (P.lift P.x ⋯)) P.X

Tactic:
by simp

Goal state after:
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
P : StandardEtalePresentation R S
⊢ X.Monic

Tactic:
by simp

Goal state after:
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
P : StandardEtalePresentation R S
⊢ derivative X * 1 + X * 0 = 1 ^ 0

Tactic:
by simp

Goal state after:
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
P : StandardEtalePresentation R S
⊢ (aeval 0) { f := X, monic_f := ⋯, g := 1, cond := ⋯ }.f = 0

Tactic:
by simp

Goal state after:
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
P : StandardEtalePresentation R S
⊢ IsUnit ((aeval 0) { f := X, monic_f := ⋯, g := 1, cond := ⋯ }.g)

Tactic:
by simp

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
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)
q : R[X]
hq : q.Monic
hqx : (aeval x) q = 0
hq'x : (aeval x) (derivative q) ∉ Q
⊢ derivative q * 1 + q * 0 = derivative q ^ 1

Tactic:
by simp

Goal state after:
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
inst✝¹ : IsStandardEtale R S
inst✝ : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective ⇑f
this✝ : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : RingHom.ker f.toRingHom = S ∙ e
⊢ S ∙ e = Ideal.span {1 - (1 - e)}

Tactic:
by simp

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
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
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hw : (mapRingHom (algebraMap R P.ResidueField)) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ p.natDegree + 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ a - a = 0

Tactic:
by simp

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

Goal state before:
pp: case inr.refine_2
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
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' : derivative m ≠ 0
c : P.ResidueField[X]
hc : Polynomial.map (algebraMap R P.ResidueField) p = m * c
⊢ ¬m ∣ derivative (Polynomial.map (algebraMap R P.ResidueField) q)

Tactic:
simp_all [hm.dvd_mul, dvd_add_left, pow_two, mul_dvd_mul_iff_left, hm.ne_zero]

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 : Q.ResidueField
hx : p.ResidueField[x] = ⊤
hx0 : x = 0
⊢ 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
⊢ (Multiset.map (fun x ↦ X - C x) m).prod ∣
    derivative (Multiset.map (fun x ↦ X - C x) m).prod * Polynomial.map (algebraMap S S') y -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum

Tactic:
derivative_prod,

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
⊢ (Multiset.map (fun x ↦ X - C x) m).prod ∣
    (Multiset.map (fun i ↦ (Multiset.map (fun x ↦ X - C x) (m.erase i)).prod * derivative (X - C i)) m).sum *
        Polynomial.map (algebraMap S S') y -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
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))
⊢ 0 < n + 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
a : S'
ham : a ∈ m
⊢ a - a = 0

Tactic:
by simp

Goal state after: