no goals
α : Type u_1
β : Type ?u.180770
γ : Type ?u.180773
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ (s ∪ t) ∩ t = t
rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_right]