no goals
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ (Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = s
rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]