Theoremseq_or_ne_mem_of_mem, list_map, list_map, exists_mem_and_apply_eq_iff, list_map, list_map, list_map, list_map, map, map_iff, of_map, imp, idxOf_eq_of_mem, idxOf_le, mem_iff_idxOf_lt_length, idxOf_add_length_le, idxOf_le, disjoint_left, disjoint_right, antisymm, cons_cons, of_cons_of_ne, append_cons_inj_of_notMem, append_eq_has_append, append_left_injective, append_right_injective, append_subset_of_subset_of_subset, bind_eq_flatMap, choose_mem, choose_property, choose_spec, comp_map, concat_eq_reverse_cons, cons_head!_tail, cons_head?_tail, cons_injective, cons_sublist_cons', cons_subset_of_subset_of_mem, disjoint_map, disjoint_pmap, disjoint_reverse_left, disjoint_reverse_right, doubleton_eq, dropLast_append_getLast, dropLast_append_getLast?, eq_cons_of_length_one, eq_cons_of_mem_head?, eq_nil_or_concat', eq_of_mem_map_const, eq_replicate_length, erase_getElem, exists_mem_cons_iff, exists_mem_cons_of, exists_mem_cons_of_exists, exists_mem_iff_get, exists_mem_iff_getElem, exists_of_length_succ, ext_getElem!, ext_getElem?', ext_getElem?_iff', ext_get_iff, filterMap_congr, filterMap_eq_flatMap_toList, filterMap_eq_map_iff_forall_eq_some, filter_attach, filter_attach', filter_comm, filter_eq_foldr, filter_false, filter_singleton, filter_subset', filter_true, flatMap_congr, flatMap_pure_eq_map, foldl1_eq_foldr1, foldlM_eq_foldl, foldl_assoc_comm_cons, foldl_concat, foldl_eq_foldr, foldl_eq_foldr', foldl_eq_of_comm', foldl_eq_of_comm_of_assoc, foldl_ext, foldl_fixed, foldl_fixed', foldl_hom₂, foldl_op_eq_op_foldr_assoc, foldrM_eq_foldr, foldr_concat, foldr_eq_of_comm', foldr_ext, foldr_fixed, foldr_fixed', foldr_hom₂, forall_append, forall_cons, forall_iff_forall_mem, forall_map_iff, forall_mem_iff_get, forall_mem_iff_getElem, forall_mem_of_forall_mem_cons, getElem?_idxOf, getElem?_length, getElem?_surjective_iff, getElem_fin_surjective_iff, getElem_map_rev, getElem_set_of_ne, getLast?_append_cons, getLast?_append_of_ne_nil, getLast?_eq_getLast_of_ne_nil, getLast?_flatten_replicate, getLastI_eq_getLast?, getLastI_eq_getLast?_getD, getLast_append_of_right_ne_nil, getLast_append_singleton, getLast_concat', getLast_congr, getLast_replicate_succ, getLast_singleton', get_attach, get_eq_getElem?, get_length_sub_one, get_reverse', get_surjective_iff, get_tail, head!_append, head!_cons, head!_eq_head?, head!_eq_head?_getD, head!_mem_head?, head!_mem_self, head!_nil, head?_append_of_ne_nil, head?_flatten_replicate, head_eq_getElem_zero, idxOf_append_of_mem, idxOf_append_of_notMem, idxOf_cons_eq, idxOf_cons_ne, idxOf_eq_length_iff, idxOf_eq_zero_iff_eq_nil_or_head_eq, idxOf_eq_zero_iff_head_eq, idxOf_get, idxOf_getLast, idxOf_inj, idxOf_of_notMem, infix_flatMap_of_mem, injective_foldl_comp, insert_neg, insert_pos, instAssociativeAppend_mathlib, instLawfulIdentityAppendNil_mathlib, instLawfulSingleton_mathlib, left_le_of_mem_range', length_eq_four, length_eq_length_filter_add, length_eq_three, length_eq_two, length_eraseIdx_add_one, length_eraseP_add_one, length_erase_add_one, length_injective, length_injective_iff, length_pos_iff_ne_nil, length_pos_of_ne_nil, lookup_graph, map_bijective_iff, map_comp_map, map_diff, map_eq_map, map_erase, map_filter, map_foldl_erase, map_injective_iff, map_involutive_iff, map_leftInverse_iff, map_reverseAux, map_rightInverse_iff, map_subset_iff, map_surjective_iff, mem_dropLast_iff_idxOf_lt, mem_dropLast_of_mem_of_ne_getLast, mem_dropLast_of_mem_of_ne_getLast?, mem_dropLast_of_mem_of_ne_getLastD, mem_filter_of_mem, mem_getLast?_append_of_mem_getLast?, mem_getLast?_cons, mem_getLast?_eq_getLast, mem_head?_append_of_mem_head?, mem_map_of_injective, mem_map_of_involutive, mem_of_mem_filter, mem_pair, mem_pure, mem_take_iff_idxOf_lt, monotone_filter_right, of_mem_filter, or_exists_of_exists_mem_cons, perm_reverse, range'_0, replicate_add, replicate_left_inj, replicate_left_injective, replicate_right_inj, replicate_right_inj', replicate_right_injective, replicate_subset_singleton, reverse_bijective, reverse_concat', reverse_cons', reverse_foldl, reverse_injective, reverse_involutive, reverse_perm', reverse_surjective, set_of_mem_cons, singleton_eq, singleton_injective, sublist_cons_of_sublist, sublist_singleton, subset_singleton_iff, succ_idxOf_lt_length_of_mem_dropLast, surjective_head!, surjective_head?, surjective_tail, tail_append_singleton_of_ne_nil | 226 |