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

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

State before:
α : Sort u_1
p : Prop
a : α
s t : Set α
⊢ (s.union (Set.pureIf a p)).union t = ((Set.pureIf a p).union s).union t
Tactic:
rw [union_comm (Set.pureIf a p) s]
State after:
no goals

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