no goals
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x : β
inst✝² : Fintype α
inst✝¹ : (a : α) → Fintype ↑(fixedBy α β a)
inst✝ : Fintype (Quotient (orbitRel α β))
⊢ ∑ a : α, Fintype.card ↑(fixedBy α β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α
rw [← Fintype.card_prod, ← Fintype.card_sigma,
  Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]