no goals
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
e : ℕ
he : e ≠ 0
hle : map f p ≤ P ^ e
hnle : ¬map f p ≤ P ^ (e + 1)
⊢ ramificationIdx f p P ≠ 0
rwa [ramificationIdx_spec hle hnle]