theorem Set.range_list_get_eq_toFinset_toSet {α : Type u_1} (l : List α) : range l.get = ↑l.toFinset

theorem Set.range_get_nil {α : Type u_1} : range [].get = ∅

theorem Set.range_get_singleton {α : Type u_1} (a : α) : range [a].get = {a}

theorem Set.range_get_cons_list {α : Type u_1} (l : List α) {a : α} : range (a :: l).get = insert a (range l.get)

theorem List.toFinset_singleton {α : Type u_1} (a : α) [DecidableEq α] : [a].toFinset = {a}