no goals
ι : Type ?u.864121
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
H : ∀ (x : α), x ∈ s → f x ∈ t
⊢ card s = ∑ a in t, card (filter (fun x => f x = a) s)
simp only [card_eq_sum_ones, sum_fiberwise_of_maps_to H]