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

State before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.insert a).inter t = ((Set.pure a).inter t).union (s.inter t)
Tactic:
rw [inter_distrib_right]
State after:
no goals

State before:
α : Sort u_1
a : α
s t : Set α
⊢ ((Set.pure a).inter t).union (s.inter t) = (Set.pureIf a (a ∈ t)).union (s.inter t)
Tactic:
rw [pure_inter]
State after:
no goals