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

State before:
α : Sort u_1
β : Sort u_2
f : α → Set β
a : α
s : Set α
⊢ (s.insert a).bind f = ((Set.pure a).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 : α
s : Set α
⊢ ((Set.pure a).bind f).union (s.bind f) = (f a).union (s.bind f)
Tactic:
rw [Set.pure_bind]
State after:
no goals