simp only [Fintype.card_ofFinset, Set.mem_univ, Finset.mem_univ, forall_true_left,
  Subtype.forall, implies_true, forall_const, Finset.filter_true_of_mem,
  MulAction.mem_stabilizer_iff, Finset.card_univ, ← Set.Nat.card_coe_set_eq,
  Nat.card_eq_fintype_card]
case pos.a
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
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ (primesOver S p).ncard * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑Set.univ * Fintype.card ↥(MulAction.stabilizer (L ≃ₐ[K] L) P)
case pos.a
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
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card ↑(primesOver S p) * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑(primesOver S p) * Fintype.card { x // x • P = P }