Theorem: isUnramifiedAt_of_Separable_minpoly (FltRegular/NumberTheory/Unramified.lean)

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
⊢ IsUnramifiedAt S p
Tactic:
rw [← IsIntegralClosure.algebraMap_mk' S x hx, minpoly.algebraMap_eq
  (IsIntegralClosure.algebraMap_injective S R L)] at h
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ IsUnramifiedAt S p

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ IsUnramifiedAt S p
Tactic:
exact isUnramifiedAt_of_Separable_minpoly' K L p hpbot (IsIntegralClosure.mk' S x hx)
  (by rwa [IsIntegralClosure.algebraMap_mk']) h
State after:
no goals

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ Algebra.adjoin K {(algebraMap S L) (IsIntegralClosure.mk' S x hx)} = ⊤
Tactic:
rwa [IsIntegralClosure.algebraMap_mk']
State after:
no goals