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

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

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