apply Finset.prod_congr rfl
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 ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P =
    ∏ p_1 ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      p_1 ^ Multiset.count p_1 (factors (Ideal.map (algebraMap R S) p))
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 ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∀ x ∈ primesOverFinset S p, x = x ^ Multiset.count x (factors (Ideal.map (algebraMap R S) p))