mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
⊢ (Spec.map (CommRingCat.ofHom ↑g₁) ≫ hV.fromSpec) ≫ f = (Spec.map (CommRingCat.ofHom ↑g₂) ≫ hV.fromSpec) ≫ f

Tactic:
by simp only [Category.assoc, ← hU.SpecMap_appLE_fromSpec f hV hVU, ← Spec.map_comp_assoc, *]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
h : IsStronglyTranscendental R x
inst✝ : FaithfulSMul R S
p : R[X]
hp : (aeval x) p = 0
⊢ ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
simpa [Algebra.smul_def, hp, Polynomial.ext_iff] using h 1 p

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

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝¹ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this✝ : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
this : ¬↑s ⊆ ↑↑I
r : S
hrs : r ∈ ↑s
hrI : r ∉ ↑↑I
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    { toRingHom := IsLocalization.map (Localization.AtPrime J) Algebra.TensorProduct.includeRight.toRingHom ⋯,
      commutes' := ⋯ }
    ⋯
hψ : ψ.comp (φ ⟨r, hrs⟩) = IsScalarTower.toAlgHom P.ResidueField (P.Fiber S) (Localization.AtPrime J)
⊢ ψ (f a ⟨r, hrs⟩) = 0

Tactic:
simp only [ha, Pi.zero_apply, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
u : S
hu : u ∈ conductor R x
hu' : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) u = y
⊢ ∃ a, ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) a = y

Tactic:
use ⟨u, conductor_subset_adjoin hu⟩

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I := ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
u : S
hu : u ∈ conductor R x
hu' : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) u = y
⊢ ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⟨u, ⋯⟩ = y
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
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ eval x (C p.leadingCoeff) * (Multiset.map (eval x) (Multiset.map (fun x ↦ X - C x) m)).prod = 0

Tactic:
Multiset.prod_eq_zero,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ eval x (C p.leadingCoeff) * 0 = 0

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ 0 ∈ Multiset.map (eval x) (Multiset.map (fun x ↦ X - C x) m)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
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
⊢ J ≤
    RingHom.ker
      ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField)))

Tactic:
simp [hJ, Ideal.map_le_iff_le_comap, RingHom.comap_ker _ C, mapRingHom_comp_C,
        RingHom.ker_comp_of_injective, C_injective,
        FaithfulSMul.algebraMap_injective I.ResidueField[X] (RatFunc I.ResidueField)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
H' : Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f) = ⊥
g' : p.ResidueField[X] ≃ₐ[p.ResidueField] p.Fiber S :=
  ((AlgEquiv.quotientBot p.ResidueField p.ResidueField[X]).symm.trans
        (Ideal.quotientEquivAlgOfEq p.ResidueField ⋯)).trans
    (fiberEquivQuotient f hf p).symm
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S)
hQ :
  (PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ }).symm Q =
    ⟨{ asIdeal := P, isPrime := inst✝¹ }, ⋯⟩
inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
⊢ False

Tactic:
exact Polynomial.not_weaklyQuasiFiniteAt (Q.asIdeal.comap g'.toRingHom) inferInstance

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
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
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ } =
    AlgHom.id I.ResidueField J.ResidueField

Tactic:
· apply AlgHom.coe_ringHom_injective
    ext
    · simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]; rfl
    · simp [f, RatFunc.liftAlgHom]

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

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst✝³ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) := (CommRingCat.Hom.hom αU).toAlgebra
algInst✝² : Algebra ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f))) := (CommRingCat.Hom.hom αUf).toAlgebra
algInst✝¹ : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst✝ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f)))))
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
have : IsScalarTower Γ(X, U.toOpens) Γ(X, X.basicOpen f) (F.obj (.op (U.basicOpen f))) :=
    .of_algebraMap_eq' congr($(α.naturality (U.basicOpen_le f).hom.op).hom).symm

Goal state after:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst✝³ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) := (CommRingCat.Hom.hom αU).toAlgebra
algInst✝² : Algebra ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f))) := (CommRingCat.Hom.hom αUf).toAlgebra
algInst✝¹ : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst✝ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f)))))
this : IsScalarTower ↑Γ(X, U.toOpens) ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f)))
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e : pullback (colimit.desc F (cocone X)) (↑U).ι ≅ ↑↑U :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ pullback.snd (colimit.desc F (cocone X)) (↑U).ι = e.hom

Tactic:
rw [← cancel_mono U.1.ι, ← Iso.inv_comp_eq]

Goal state after:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e : pullback (colimit.desc F (cocone X)) (↑U).ι ≅ ↑↑U :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ e.inv ≫ pullback.snd (colimit.desc F (cocone X)) (↑U).ι ≫ (↑U).ι = (↑U).ι
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H.hb
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑(q * q') ≠ 0

pp: case inr.H.H.hd
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q * φ ↑q' ≠ 0

pp: case inr.H.H.hb
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q ≠ 0

pp: case inr.H.H.hd
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q' ≠ 0

Tactic:
all_goals
        try simp only [← map_mul, ← Submonoid.coe_mul]
        exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

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⁰
r : S
⊢ (↑↑(liftRingHom φ.toRingHom hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S L) r

Tactic:
simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x * y = (algebraMap K[X] K⟮X⟯) (x.num * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
by
    conv_lhs =>
      rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
q : K[X]
hq : q ≠ 0
p : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom ∣ q

Tactic:
exact denom_div_dvd p q

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.num ∣ x.denom

Tactic:
by
  rw [num_dvd x.denom_ne_zero]
  refine ⟨x.num, num_ne_zero hx, ?_⟩
  nth_rw 1 [← x.num_div_denom]
  rw [inv_div]

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
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 := Localization.Away ((AdjoinRoot.mk P.f) P.g)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away ((AdjoinRoot.mk P.f) (p * P.g))
    (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
⊢ IsStandardEtale R Sₛ

Tactic:
have H : Submonoid.map e.symm.toRingEquiv.toMonoidHom (.powers
      (algebraMap _ S' (AdjoinRoot.mk P.f p))) = .powers (aeval P.x p) := by
    have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
    rw [Submonoid.map_powers]
    exact congr(Submonoid.powers ($this p))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 := Localization.Away ((AdjoinRoot.mk P.f) P.g)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away ((AdjoinRoot.mk P.f) (p * P.g))
    (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
H :
  Submonoid.map e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p))) =
    Submonoid.powers ((aeval P.x) p)
⊢ IsStandardEtale R Sₛ
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
q : R[X]
n : ℕ
hn : IsIntegral R (p.leadingCoeff ^ n • (t * x) - φ q)
r : R
hr : (algebraMap R S) r = p.leadingCoeff ^ n • (t * x) - φ q
⊢ φ.toRingHom (C r + q) = p.leadingCoeff ^ n • (t * x)

Tactic:
by simp [← Polynomial.algebraMap_eq, -Polynomial.algebraMap_apply, hr]

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

Goal state before:
pp: case e'_3
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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
y : B[X]
hy : (AdjoinRoot.mk 𝓟'.f) (derivative 𝓟'.f) * ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a) = (AdjoinRoot.mk 𝓟'.f) y
hRy : ∀ (i : ℕ), IsIntegral R (y.coeff i)
⊢ eval₂ Algebra.TensorProduct.includeRight.toRingHom (𝓟.x ⊗ₜ[R] 1) y =
    (Algebra.TensorProduct.comm R B S)
      (e.symm ((algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) y)))

Tactic:
simp only [← AlgEquiv.coe_toAlgHom, ← AlgHom.coe_toRingHom, ← RingHom.comp_apply,
        ← coe_eval₂RingHom]
      congr 1
      ext <;> simp [e, StandardEtalePair.equivAwayAdjoinRoot]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ (-1) ^ (m * n) * (0 ^ n * g.coeff 0 ^ m) = 0 ^ n * g.coeff 0 ^ m

Tactic:
cases n <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
b : Fin (m + 1 + (n + 1))
hb : b ≠ Fin.castAdd (n + 1) (Fin.last m)
this : f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) b = 0
⊢ (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑b) * f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) b *
      ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove b.succAbove).det =
    0

Tactic:
by simp [this]

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

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

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hg]

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

Goal state before:
pp: case pos
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
⊢ (g * r).resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
rw [← resultant_add_mul_left _ _ (-r) _ _ _ le_rfl]

Goal state after:
case pos
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
⊢ (g * r + g * -r).resultant g (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

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
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree