Theorem: isUnramifiedAt_of_Separable_minpoly'
Proof 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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Tactic:
apply le_antisymm
Proof state after:
case a
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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ Ideal.ramificationIdx (algebraMap R S) p P ≤ 1

case a
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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ 1 ≤ Ideal.ramificationIdx (algebraMap R S) p P