Theorem: Ideal.ramificationIdxIn_bot (FltRegular/NumberTheory/GaloisPrime.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
⊢ ramificationIdxIn S ⊥ = 0
Tactic:
delta ramificationIdxIn
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
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0

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
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
by_cases h : (primesOver S (⊥ : Ideal R)).Nonempty
State after:
case pos
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
h : (primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0

case neg
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
h : ¬(primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0

State before:
case pos
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
h : (primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
rw [dif_pos h, ramificationIdx_bot]
State after:
no goals

State before:
case neg
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
h : ¬(primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
exact dif_neg h
State after:
no goals