no goals
ι : Type ?u.99968
α : Type u_1
β : Type u_2
M : Type ?u.99977
N : Type ?u.99980
G : Type ?u.99983
k : Type ?u.99986
R : Type ?u.99989
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → n ≤ card (filter (fun x => f x = a) s)
⊢ n * card t = ∑ _a in t, n
simp [mul_comm]
no goals
ι : Type ?u.99968
α : Type u_1
β : Type u_2
M : Type ?u.99977
N : Type ?u.99980
G : Type ?u.99983
k : Type ?u.99986
R : Type ?u.99989
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → n ≤ card (filter (fun x => f x = a) s)
⊢ ∑ a in t, card (filter (fun x => f x = a) s) = card s
rw [← card_eq_sum_card_fiberwise Hf]