∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match hkky : compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLED k r (ky, y)
      | Ordering.eq => (ky, y)
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryLE k l ⋯ ⋯