rw [dif_pos h, ramificationIdx_bot]
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
no goals