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

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

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