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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
⊢ IsUnramifiedAt S p
Tactic:
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ 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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ IsUnramifiedAt S p
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
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 : 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)
⊢ 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 : 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)
⊢ IsUnramifiedAt S p
Tactic:
have := NoZeroSMulDivisors.iff_algebraMap_injective.mpr hRS
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isNoetherian R K L S
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isDedekindDomain R K L S
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
have := aeval_derivative_mem_differentIdeal R K L x hx'
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
have H : RingHom.comp (algebraMap (FractionRing R) (FractionRing S))
  ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    RingHom.comp ↑(FractionRing.algEquiv S L).symm.toRingEquiv (algebraMap K L) := by
  apply IsLocalization.ringHom_ext R⁰
  ext
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
    ← IsScalarTower.algebraMap_apply]
  rw [IsScalarTower.algebraMap_apply R S L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
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 : 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)
⊢ 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 : 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)
⊢ IsUnramifiedAt S p
Tactic:
have : IsSeparable (FractionRing R) (FractionRing S) := IsSeparable.of_equiv_equiv _ _ 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 : 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)
⊢ 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 : 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)
⊢ IsUnramifiedAt S p
Tactic:
have := hp.isMaximal hpbot
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 : 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
⊢ 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 : 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
⊢ IsUnramifiedAt S p
Tactic:
intro P hP
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 : 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
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1

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
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Tactic:
letI : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
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 : 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
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1

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
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Tactic:
have := isMaximal_of_mem_primesOver hpbot hP
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 : 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

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
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

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
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_
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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))

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
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
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 : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this : IsDomain S
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
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 : 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
⊢ (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
Tactic:
apply IsLocalization.ringHom_ext R⁰
State after:
case h
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
⊢ ((algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv).comp
      (algebraMap R K) =
    ((↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)

State before:
case h
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
⊢ ((algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv).comp
      (algebraMap R K) =
    ((↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)
Tactic:
ext
State after:
case h.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
x✝ : R
⊢ (((algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv).comp
        (algebraMap R K))
      x✝ =
    (((↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)) x✝

State before:
case h.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
x✝ : R
⊢ (((algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv).comp
        (algebraMap R K))
      x✝ =
    (((↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)) x✝
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
  AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
  ← IsScalarTower.algebraMap_apply]
State after:
case h.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
x✝ : R
⊢ (algebraMap R (FractionRing S)) x✝ = (FractionRing.algEquiv S L).symm ((algebraMap R L) x✝)

State before:
case h.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
x✝ : R
⊢ (algebraMap R (FractionRing S)) x✝ = (FractionRing.algEquiv S L).symm ((algebraMap R L) x✝)
Tactic:
rw [IsScalarTower.algebraMap_apply R S L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
State after:
no goals

State before:
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
Tactic:
rw [← tsub_eq_zero_iff_le]
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 = 0

State before:
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 = 0
Tactic:
by_contra H
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ False

State before:
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ False
Tactic:
have hxP : aeval x (derivative (minpoly R x)) ∈ P := by
  have : differentIdeal R S ≤ P := by
    rw [← Ideal.dvd_iff_le]
    exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
    (Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R S)))
  exact this (aeval_derivative_mem_differentIdeal R K L _ hx')
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (aeval x) (derivative (minpoly R x)) ∈ P
⊢ False

State before:
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (aeval x) (derivative (minpoly R x)) ∈ P
⊢ False
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hxP
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
⊢ False

State before:
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
⊢ False
Tactic:
have := (separable_map (Ideal.quotientMap P (algebraMap R S) hP.2.ge)).mpr h
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
this : (map (Ideal.quotientMap P (algebraMap R S) ⋯) (map (Ideal.Quotient.mk p) (minpoly R x))).Separable
⊢ False

State before:
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
this : (map (Ideal.quotientMap P (algebraMap R S) ⋯) (map (Ideal.Quotient.mk p) (minpoly R x))).Separable
⊢ False
Tactic:
rw [map_map, Ideal.quotientMap_comp_mk] at this
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
this : (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x)).Separable
⊢ False

State before:
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
this : (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x)).Separable
⊢ False
Tactic:
obtain ⟨a, b, e⟩ := this
State after:
case a.intro.intro
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
a b : (S ⧸ P)[X]
e :
  a * map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x) +
      b * derivative (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x)) =
    1
⊢ False

State before:
case a.intro.intro
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
a b : (S ⧸ P)[X]
e :
  a * map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x) +
      b * derivative (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x)) =
    1
⊢ False
Tactic:
apply_fun (aeval (Ideal.Quotient.mk P x)) at e
State after:
case a.intro.intro
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
a b : (S ⧸ P)[X]
e :
  (aeval ((Ideal.Quotient.mk P) x))
      (a * map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x) +
        b * derivative (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x))) =
    (aeval ((Ideal.Quotient.mk P) x)) 1
⊢ False

State before:
case a.intro.intro
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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
hxP : (algebraMap S (S ⧸ P)) ((aeval x) (derivative (minpoly R x))) = 0
a b : (S ⧸ P)[X]
e :
  (aeval ((Ideal.Quotient.mk P) x))
      (a * map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x) +
        b * derivative (map ((Ideal.Quotient.mk P).comp (algebraMap R S)) (minpoly R x))) =
    (aeval ((Ideal.Quotient.mk P) x)) 1
⊢ False
Tactic:
simp_rw [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul,
  aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, hxP, map_zero, mul_zero,
  zero_add, map_one, zero_ne_one] at e
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 : 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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ (aeval x) (derivative (minpoly R x)) ∈ P
Tactic:
have : differentIdeal R S ≤ P := by
  rw [← Ideal.dvd_iff_le]
  exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
  (Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R S)))
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 : 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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
this : differentIdeal R S ≤ P
⊢ (aeval x) (derivative (minpoly R x)) ∈ 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 : 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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
this : differentIdeal R S ≤ P
⊢ (aeval x) (derivative (minpoly R x)) ∈ P
Tactic:
exact this (aeval_derivative_mem_differentIdeal R K L _ hx')
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 : 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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ differentIdeal R S ≤ P
Tactic:
rw [← Ideal.dvd_iff_le]
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 : 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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ P ∣ differentIdeal R S

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
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ P ∣ differentIdeal R S
Tactic:
exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
(Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R S)))
State after:
no goals

State before:
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
Tactic:
rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _
  (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP),
  Multiset.one_le_count_iff_mem, ← Multiset.mem_toFinset, ← primesOverFinset,
  ← Finset.mem_coe, coe_primesOverFinset _ p hpbot]
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 : 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.map (algebraMap R 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 : 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.map (algebraMap R S) p ≠ ⊥
Tactic:
rwa [ne_eq, Ideal.map_eq_bot_iff_of_injective hRS]
State after:
no goals