mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : Field L
φ : K[X] →+* L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
x : K[X]
⊢ (liftRingHom φ hφ) ((algebraMap K[X] K⟮X⟯) x) = φ x

Tactic:
simpa using

Goal state after:
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : Field L
φ : K[X] →+* L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
x : K[X]
⊢ (liftRingHom φ hφ) ((algebraMap K[X] K⟮X⟯) x) = φ x
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : K⟮X⟯ → Prop
x : K⟮X⟯
f : ∀ (p q : K[X]), q ≠ 0 → P ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
p q : K[X]
hq : q ≠ 0
⊢ P (RatFunc.mk p q)

Tactic:
simpa using

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : K⟮X⟯ → Prop
x : K⟮X⟯
f : ∀ (p q : K[X]), q ≠ 0 → P ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
p q : K[X]
hq : q ≠ 0
⊢ P ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
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 : S
h : P.HasMap x
f : S →ₐ[R] T
⊢ IsUnit ((aeval (f x)) P.g)

Tactic:
simpa using

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
P : StandardEtalePair R
x : S
h : P.HasMap x
f : S →ₐ[R] T
⊢ IsUnit (f ((aeval x) P.g))
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
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ (aeval x) P.g ^ n = (aeval x) (derivative P.f) * ?m.78

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ (aeval x) P.g ^ n = (aeval x) (derivative P.f) * ?m.78
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
convert! num_div (1 : K[X]) 1 <;> simp

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

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

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ¬q / gcd p q = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
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).leadingCoeff⁻¹ ≠ 0

Tactic:
simpa using

Goal state after:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ¬q / gcd p q = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq

Goal state after:
case f
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⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num /
      (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval (x + (aeval x) P.f * -b)) P.f = 0

Tactic:
rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (by grind)]; grind

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

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

Tactic:
exact num_div_dvd p hq

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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
ε : S
H : ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
y : { x // P.HasMap x }
hy : (fun a ↦ ↑a - x ∈ I) y
⊢ P.HasMap (x + (↑y - x))

Tactic:
simpa using

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
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
ε : S
H : ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
y : { x // P.HasMap x }
hy : (fun a ↦ ↑a - x ∈ I) y
⊢ P.HasMap ↑y
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_3
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
⊢ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f} ≤ RingHom.ker (IsLocalization.Away.liftAlgHom P.g ⋯)

Tactic:
simpa using

Goal state after:
case refine_3
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
⊢ (aeval P.X) P.f = 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
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)

Tactic:
simpa using

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
⊢ (IsLocalization.Away.lift ((AdjoinRoot.mk P.f) P.g) ⋯) x * (aeval P.X) P.g ^ n = (aeval P.X) p
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 R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝³ : Q'.LiesOver Q
this✝² : Q'.LiesOver P
this✝¹ : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this : IsUnramifiedAt P.ResidueField Q'
⊢ P.ResidueField[1 ⊗ₜ[R] x] = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝³ : Q'.LiesOver Q
this✝² : Q'.LiesOver P
this✝¹ : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this : IsUnramifiedAt P.ResidueField Q'
⊢ P.ResidueField[1 ⊗ₜ[R] x] = ⊤
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
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
⊢ P.HasMap (P.map (algebraMap R T)).X

Tactic:
simpa using

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
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
⊢ (aeval (P.map (algebraMap R T)).X) P.f = 0 ∧ IsUnit ((aeval (P.map (algebraMap R T)).X) P.g)
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
P : StandardEtalePair R
⊢ Function.Bijective ⇑(P.lift P.X ⋯)

Tactic:
simpa using

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
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R
⊢ Function.Bijective _root_.id
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
P : StandardEtalePair R := { f := q, monic_f := hq, g := derivative q, cond := ⋯ }
⊢ IsUnit ((aeval ((algebraMap S (Localization.Away ((aeval x) (derivative q)))) x)) P.g)

Tactic:
simpa using

Goal state after:
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
P : StandardEtalePair R := { f := q, monic_f := hq, g := derivative q, cond := ⋯ }
⊢ IsUnit ((algebraMap S (Localization.Away ((aeval x) (derivative q)))) ((aeval x) P.g))
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
P : StandardEtalePair R := { f := q, monic_f := hq, g := derivative q, cond := ⋯ }
hP : P.HasMap ((algebraMap S (Localization.Away ((aeval x) (derivative q)))) x)
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
this : IsLocalization.Away ((aeval x) (derivative q)) (Localization.Away (f ((AdjoinRoot.mk P.f) P.g)))
⊢ Function.Surjective ⇑((Localization.awayMapₐ f ((AdjoinRoot.mk P.f) P.g)).comp ↑P.equivAwayAdjoinRoot)

Tactic:
simpa using

Goal state after:
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
P : StandardEtalePair R := { f := q, monic_f := hq, g := derivative q, cond := ⋯ }
hP : P.HasMap ((algebraMap S (Localization.Away ((aeval x) (derivative q)))) x)
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
this : IsLocalization.Away ((aeval x) (derivative q)) (Localization.Away (f ((AdjoinRoot.mk P.f) P.g)))
⊢ Function.Surjective ⇑(Localization.awayMapₐ f ((AdjoinRoot.mk P.f) P.g))
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ₛ
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)))))
r : R
⊢ (IsLocalization.ringEquivOfRingEquiv (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p))) Sₛ
          e.symm.toRingEquiv H).toFun
      ((algebraMap R (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))) r) =
    (algebraMap R Sₛ) r

Tactic:
by
        simp [IsScalarTower.algebraMap_apply R S' (Localization.Away _),
          - AlgEquiv.symm_toRingEquiv, IsScalarTower.algebraMap_eq R S Sₛ]

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 ⇑φ
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hf : Monic 1
hf' : ∀ (i : ℕ), IsIntegral R (coeff 1 i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {1}
⊢ False

Tactic:
simpa using

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 ⇑φ
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hf : Monic 1
hf' : ∀ (i : ℕ), IsIntegral R (coeff 1 i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {1}
⊢ False
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 ⇑φ
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hf : Monic 1
hf' : ∀ (i : ℕ), IsIntegral R (coeff 1 i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {1}
⊢ False

Tactic:
simpa using (RingHom.ker_ne_top φ.toRingHom).symm.trans_eq hfx

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

Goal state before:
pp: case refine_2
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
⊢ IsIntegral R 0

pp: case refine_2
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
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)

Tactic:
· exact isIntegral_zero

Goal state after:
case refine_2
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
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case refine_2
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
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)

Tactic:
simpa using

Goal state after:
case refine_2
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_1 ∈ m, a - a_1 = 0