classical
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
apply Finset.prod_congr rfl
intros P hP
convert (pow_one _).symm
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count hpbot' hP.1
  (ne_bot_of_mem_primesOver hp hP)]
exact IsUnramified.isUnramifiedAt _ hp _ 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✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
no goals