feat: add Insert instances for NameMap/NameSet (#14153)

This PR adds `Insert` instances for `NameMap` and `NameSet`.

Author: Vtec234

src/Lean/Data/NameMap/Basic.lean

@@ -35,6 +35,9 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.TreeMap.contains m n
 
 def find? (m : NameMap α) (n : Name) : Option α := Std.TreeMap.get? m n
 
+instance : Insert (Name × α) (NameMap α) where
+  insert e s := s.insert e.1 e.2
+
 instance [Monad m] : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
 
@@ -52,6 +55,8 @@ instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨empty⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.TreeSet.insert s n
 def contains (s : NameSet) (n : Name) : Bool := Std.TreeSet.contains s n
+instance : Insert Name NameSet where
+  insert n s := s.insert n
 instance [Monad m] : ForIn m NameSet Name :=
   inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)