Theorem: Set.insert_union_left (GMLInit/Data/Set/Insert.lean)

State before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.insert a).union t = (Set.pure a).union (s.union t)
Tactic:
rw [union_assoc]
State after:
no goals