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

State before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
p : Prop
s : Set α
⊢ Set.map f (s.insertIf a p) = (Set.map f (Set.pureIf a p)).union (Set.map f s)
Tactic:
rw [union_map]
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
p : Prop
s : Set α
⊢ (Set.map f (Set.pureIf a p)).union (Set.map f s) = (Set.pureIf (f a) p).union (Set.map f s)
Tactic:
rw [Set.map_pureIf]
State after:
no goals