rw [insert_eq, insert_eq, ← inter_union_distrib_right, Disjoint.inter_eq _, empty_union]
α : Type u_1
ι : Type u_2
A : Set α
b c : α
hne : b ≠ c
⊢ insert b A ∩ insert c A = A
α : Type u_1
ι : Type u_2
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}