∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S}
  [inst_3 : p.IsPrime] [IsNoetherianRing S] [Algebra.IsUnramifiedAt R p],
  p ≠ ⊥ → ∀ [IsDomain S] [Algebra.EssFiniteType R S], (Ideal.under R p).ramificationIdx p = 1