mathlib-initiative/mathlib-tactics huggingface dataset:
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
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)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ (fun x ↦ C ((algebraMap R I.ResidueField) s) * x) x = (fun x ↦ C ((algebraMap R I.ResidueField) s) * x) 0

Tactic:
simp only [← algebraMap_eq, ← Algebra.smul_def]

Goal state after:
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
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)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ (algebraMap R I.ResidueField) s • x = (algebraMap R I.ResidueField) s • 0
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
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)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ (algebraMap R I.ResidueField) s • x = (algebraMap R I.ResidueField) s • 0

Tactic:
algebraMap_smul

Goal state after:
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
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)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ s • x = (algebraMap R I.ResidueField) s • 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})

Tactic:
refine ⟨fun _ ↦ f.isDiscrete_preimage_singleton, fun H ↦ ?_⟩
  change id _ -- avoid typeclass synthesis from getting stuck on the wlog hypothesis.
  wlog hY : ∃ R, Y = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
    convert!
      (H (Y.affineCover.f i x)).preimage ((pullback.fst f _).continuous.continuousOn)
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective
    ext
    simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ (fun x ↦ (H x).preimage (X.affineCover.f _).continuous.continuousOn
      (X.affineCover.f _).isOpenEmbedding.injective) ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  simp only [HasRingHomProperty.Spec_iff, id_eq] at *
  algebraize [φ.hom]
  exact (Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr fun x ↦
    ((Spec.map φ).isCompact_preimage_singleton _).finite (H _)

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
⊢ (relativeGluingData H).toBase ⁻¹ᵁ ↑U = Hom.opensRange ((relativeGluingData H).cover.f U)

Tactic:
by
  simpa using! (relativeGluingData H).toBase_preimage_eq_opensRange_ι U

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

Goal state before:
pp: case inr.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]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
y : FractionRing R[X]
pq : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      ({ toFractionRing := Localization.mk pq.1 pq.2 } + { toFractionRing := y }) =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk pq.1 pq.2 } +
      (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := y }

Tactic:
cases y using Localization.induction_on with | _ p'q'
       =>  _ 

Goal state after:
case inr.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]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
pq p'q' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      ({ toFractionRing := Localization.mk pq.1 pq.2 } + { toFractionRing := Localization.mk p'q'.1 p'q'.2 }) =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk pq.1 pq.2 } +
      (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk p'q'.1 p'q'.2 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
⊢ C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * p / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Tactic:
have hdivp : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ p :=
        (C_mul_dvd hainv).mpr (gcd_dvd_left p q)

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
⊢ C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * p / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
by
  rw [num, numDenom_div _ hq]

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

Goal state before:
pp: case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Tactic:
refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)

Goal state after:
case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ ¬(q / gcd p q).leadingCoeff⁻¹ = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * 1

pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

Tactic:
mul_one,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom

case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x = (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * 1

pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) p ≠ 0

Tactic:
mul_one,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x = (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom

case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) p ≠ 0
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 : StandardEtalePresentation R S
⊢ P.toSubmersivePresentation.jacobian = (aeval P.x) (derivative P.f) * (aeval P.x) P.g

Tactic:
by
  simp [StandardEtalePresentation.toSubmersivePresentation]

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 : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
r : ↑s
⊢ IsLocalizedModule.Away (↑r)
    (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap

Tactic:
let := (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r))
      (AlgHom.id R (integralClosure R B))).toAlgebra

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 : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
r : ↑s
this : Algebra (S ⊗[R] ↥(integralClosure R B)) (Sᵣ r ⊗[R] ↥(integralClosure R B)) :=
  (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toAlgebra
⊢ IsLocalizedModule.Away (↑r)
    (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
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 : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
n : ℕ
p : R[X]
e :
  x *
      (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
        ↑((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).2 =
    (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
      ((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).1
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.x) p

Tactic:
refine ⟨p, n, P.equivRing.injective ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
n : ℕ
p : R[X]
e :
  x *
      (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
        ↑((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).2 =
    (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
      ((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).1
⊢ P.equivRing ((P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n) = P.equivRing ((aeval P.x) p)
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)))
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)
this : IsLocalization.Away ((aeval P.x) p) Sₛ
⊢ IsStandardEtale R Sₛ

Tactic:
let e₁ : P'.Ring ≃ₐ[R]
      Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)) :=
    P'.equivAwayAdjoinRoot.trans ((IsLocalization.algEquiv (.powers (AdjoinRoot.mk P.f (p * P.g)))
      (Localization.Away (AdjoinRoot.mk P.f (p * P.g))) _).restrictScalars R)

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)
this : IsLocalization.Away ((aeval P.x) p) Sₛ
e₁ : P'.Ring ≃ₐ[R] Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)) :=
  P'.equivAwayAdjoinRoot.trans
    (AlgEquiv.restrictScalars R
      (IsLocalization.algEquiv (Submonoid.powers ((AdjoinRoot.mk P.f) (p * P.g)))
        (Localization.Away ((AdjoinRoot.mk P.f) (p * P.g)))
        (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))))
⊢ IsStandardEtale R Sₛ
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
⊢ IsStandardEtale R T

Tactic:
obtain ⟨e, he, hfe⟩ :=
    (Ideal.isIdempotentElem_iff_of_fg _ (Algebra.FinitePresentation.ker_fG_of_surjective f hf)).mp
      ((Algebra.FormallyEtale.iff_of_surjective hf).mp (.of_restrictScalars (R := R)))

Goal state after:
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
⊢ IsStandardEtale R T
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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
have : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_›
      ((Ideal.disjoint_powers_iff_notMem_of_isPrime _).mpr hfp)

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) =
    ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) PQ.1 + (LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2))

Tactic:
rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]

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

Goal state before:
pp: case e'_5
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)
⊢ ((aeval 𝓟.x) (derivative 𝓟.f) * ((aeval 𝓟.x) 𝓟.g ^ k * (aeval 𝓟.x) 𝓟.g ^ m)) •
      (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, ⋯⟩)) =
    eval₂ Algebra.TensorProduct.includeRight.toRingHom (𝓟.x ⊗ₜ[R] 1) y

Tactic:
convert! congr(Algebra.TensorProduct.comm _ _ _ <| e.symm (algebraMap _ _ $hy))
    · apply (Algebra.TensorProduct.comm R B S).symm.injective
      apply e.injective
      simp only [Algebra.smul_def, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
        RingHom.id_apply, map_mul, Algebra.TensorProduct.comm_symm_tmul, AlgEquiv.symm_apply_apply,
        AlgEquiv.apply_symm_apply, map_pow, heg]
      simp_rw [mul_assoc, ← map_pow, show 𝓟.g.map (algebraMap R B) = 𝓟'.g from rfl,
        IsLocalization.mk'_spec'_mk, ← derivative_map]; rfl
    · 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
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * p) m n = f.resultant g m n

Tactic:
← p.sum_monomial_eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * p.sum fun n a ↦ (monomial n) a) m n = f.resultant g m n