∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {f : α → Bool} {k : α}, (Std.ExtTreeSet.filter f t).get! k = (Option.filter f (t.get? k)).get!