∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α) [inst_1 : Inhabited α],
  t.getKey! k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getKey!" 186 13
        "Key is not present in map"
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match compare k k' with
      | Ordering.lt => l.getKey! k
      | Ordering.gt => r.getKey! k
      | Ordering.eq => k'