refactor: move Inhabited instances in constant DTreeMap queries (#11448)

This PR moves the `Inhabited` instances in constant `DTreeMap` (and
related) queries, such as `Const.get!`, where the `Inhabited` instance
can be provided before proving a key.

Author: wkrozowski

src/Std/Data/DTreeMap/Basic.lean

@@ -685,7 +685,7 @@ def get (t : DTreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
 
 @[inline, inherit_doc DTreeMap.get!]
-def get! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
+def get! [Inhabited β] (t : DTreeMap α β cmp) (a : α) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
 
 @[inline, inherit_doc DTreeMap.getD]

src/Std/Data/DTreeMap/Internal/Queries.lean

@@ -216,7 +216,7 @@ def get [Ord α] (t : Impl α δ) (k : α) (hlk : t.contains k = true) : δ :=
     | .eq => v'
 
 /-- Returns the value for the key `k`, or panics if such a key does not exist. -/
-def get! [Ord α] (t : Impl α δ) (k : α) [Inhabited δ] : δ :=
+def get! [Ord α] [Inhabited δ] (t : Impl α δ) (k : α) : δ :=
   match t with
   | .leaf => panic! "Key is not present in map"
   | .inner _ k' v' l r =>

src/Std/Data/DTreeMap/Raw/Basic.lean

@@ -433,7 +433,7 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
 
 @[inline, inherit_doc DTreeMap.Const.get!]
-def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
+def get! [Inhabited β] (t : Raw α β cmp) (a : α) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
 
 @[inline, inherit_doc DTreeMap.Const.getD]

src/Std/Data/ExtDTreeMap/Basic.lean

@@ -521,7 +521,7 @@ def get [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β :
     (fun _ _ _ _ h => h.constGet_eq)
 
 @[inline, inherit_doc ExtDTreeMap.get!]
-def get! [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) [Inhabited β] : β :=
+def get! [TransCmp cmp] [Inhabited β] (t : ExtDTreeMap α β cmp) (a : α) : β :=
   t.lift (fun m => DTreeMap.Const.get! m a)
     (fun _ _ h => h.constGet!_eq)
 

src/Std/Data/ExtTreeMap/Basic.lean

@@ -152,7 +152,7 @@ def get [TransCmp cmp] (t : ExtTreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
   ExtDTreeMap.Const.get t.inner a h
 
 @[inline, inherit_doc ExtDTreeMap.Const.get!]
-def get! [TransCmp cmp] (t : ExtTreeMap α β cmp) (a : α) [Inhabited β] : β :=
+def get! [TransCmp cmp] [Inhabited β] (t : ExtTreeMap α β cmp) (a : α) : β :=
   ExtDTreeMap.Const.get! t.inner a
 
 @[inline, inherit_doc ExtDTreeMap.Const.getD]

src/Std/Data/TreeMap/Basic.lean

@@ -155,7 +155,7 @@ def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
   DTreeMap.Const.get t.inner a h
 
 @[inline, inherit_doc DTreeMap.Const.get!]
-def get! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
+def get! [Inhabited β] (t : TreeMap α β cmp) (a : α) : β :=
   DTreeMap.Const.get! t.inner a
 
 @[inline, inherit_doc DTreeMap.Const.getD]

src/Std/Data/TreeMap/Raw/Basic.lean

@@ -167,7 +167,7 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   DTreeMap.Raw.Const.get t.inner a h
 
 @[inline, inherit_doc DTreeMap.Raw.Const.get!]
-def get! (t : Raw α β cmp) (a : α) [Inhabited β]  : β :=
+def get! [Inhabited β] (t : Raw α β cmp) (a : α) : β :=
   DTreeMap.Raw.Const.get! t.inner a
 
 @[inline, inherit_doc DTreeMap.Raw.Const.getD]