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

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

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