no goals
ι : Type ?u.97925
α : Type u_1
β : Type u_2
M : Type ?u.97934
N : Type ?u.97937
G : Type ?u.97940
k : Type ?u.97943
R : Type ?u.97946
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → card (filter (fun x => f x = a) s) ≤ n
⊢ ∑ _a in t, n = n * card t
simp [mul_comm]