Theorem: Set.union_insert_eq (Matroid/ForMathlib/Set.lean)

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