no goals
α : Type u_2
β : Type u_1
γ : Type ?u.102529
ι : Sort ?u.102532
ι' : Sort ?u.102535
ι₂ : Sort ?u.102538
κ : ι → Sort ?u.102543
κ₁ : ι → Sort ?u.102548
κ₂ : ι → Sort ?u.102553
κ' : ι' → Sort ?u.102558
a b : α
s : α → Set β
⊢ (⋂ (x : α) (_ : x ∈ {a, b}), s x) = s a ∩ s b
rw [biInter_insert, biInter_singleton]