classical
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
have := IsIntegralClosure.isDedekindDomain R K L S
have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
have := IsIntegralClosure.isNoetherian R K L S
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 _ _)
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hRS
rw [← Ideal.sum_ramification_inertia (S := S) p K L hp, ← coe_primesOverFinset S p hp,
  Set.ncard_coe_Finset, mul_comm, ← smul_eq_mul, ← Finset.sum_const]
apply Finset.sum_congr rfl
simp_rw [← Finset.mem_coe, coe_primesOverFinset S p hp]
intro P hP
rw [Ideal.ramificationIdxIn_eq_ramificationIdx K L p P hP,
  Ideal.inertiaDegIn_eq_inertiaDeg K L p P hP]
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✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
no goals