∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (hlk : k ∈ t),
  t.get k hlk =
    match t, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk =>
      match h : compare k k' with
      | Ordering.lt => l.get k ⋯
      | Ordering.gt => r.get k ⋯
      | Ordering.eq => cast ⋯ v'