no goals
α : Type u_1
β : Type ?u.174037
γ : Type ?u.174040
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u✝ v : Finset α
a b : α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
simp (config := { contextual := true }) [subset_iff, mem_inter]