no goals
α : Type u_1
β : Type u_2
γ : Type ?u.521487
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
⊢ (Finset.biUnion t fun a => filter (fun c => f c = a) s) = s
simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h