Renaming theorems related to sets

Stream: mathlib4

[Jihoon Hyun]

As we were working on #17413 , there seemed to be some naming issues with theorems on set-related data types, for example docs4#Finset.Insert.comm , or the collisions with docs4#Multiset.cons_swap and docs4#Set.insert_comm . @Eric Wieser suggested to make a thread for it, and here it is.

[Eric Wieser]

(in case anyone was wondering, docs3#finset.insert.comm was the lean 3 name which also has a strangely-placed .)