no goals
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x b : β
inst✝² : Fintype α
inst✝¹ : Fintype ↑(orbit α b)
inst✝ : Fintype { x // x ∈ stabilizer α b }
⊢ Fintype.card ↑(orbit α b) * Fintype.card { x // x ∈ stabilizer α b } = Fintype.card α
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]