rw [insert_eq, insert_eq, ← union_union_distrib_right, @union_comm _ {b} _,
  union_assoc, ← insert_eq, ← insert_eq]
α : Type u_1
A : Set α
b c : α
⊢ insert b A ∪ insert c A = insert c (insert b A)
no goals