ink

theorem Mt.Utils.List.get_in {T : Type u} (l : List T) (idx : Fin (List.length l)) : List.get l idx ∈ l

ink

theorem Mt.Utils.List.get_of_set {T : Type u} (l : List T) (idx : Nat) (a : T) (isLt : idx < List.length (List.set l idx a)) : List.get (List.set l idx a) { val := idx, isLt := isLt } = a

ink

theorem Mt.Utils.List.erase_subset {T : Type u} {a : T} (l : List T) (idx : Nat) : a ∈ List.eraseIdx l idx → a ∈ l

ink

theorem Mt.Utils.List.set_subset {T : Type u} {a : T} (l : List T) (idx : Nat) (new_value : T) : a ∈ List.set l idx new_value → a = new_value ∨ a ∈ l

ink

theorem Mt.Utils.List.index_exists {T : Type u} {a : T} (l : List T) : a ∈ l → ∃ i, List.get l i = a

ink

theorem Mt.Utils.List.erase_set {T : Type u} (l : List T) (idx : Nat) (new_value : T) : List.eraseIdx (List.set l idx new_value) idx = List.eraseIdx l idx

ink

theorem Mt.Utils.List.eq_of_in_map {U : Type u} {V : Type u} {f : U → V} {l : List U} {v : V} : v ∈ List.map f l → ∃ u, u ∈ l ∧ v = f u

ink

theorem Mt.Utils.List.get_congr {T : Type u} {l : List T} {l' : List T} (idx : Fin (List.length l)) (eq : l = l') : List.get l idx = List.get l' (Mt.Utils.Fin.cast idx (_ : List.length l = List.length l'))

ink

theorem Mt.Utils.List.get_congr' {T : Type u} {l : List T} {l' : List T} {i : Fin (List.length l)} {j : Fin (List.length l')} (l_eq : l = l') (i_eq : i.val = j.val) : List.get l i = List.get l' j

ink

theorem Mt.Utils.List.get_of_map {U : Type u} {V : Type u} {f : U → V} {l : List U} {idx : Fin (List.length (List.map f l))} : List.get (List.map f l) idx = f (List.get l (Mt.Utils.Fin.cast idx (_ : List.length (List.map f l) = List.length l)))

ink

theorem Mt.Utils.List.set_map_commutes {U : Type u} {V : Type u} (f : U → V) (l : List U) (idx : Nat) (new_val : U) : List.map f (List.set l idx new_val) = List.set (List.map f l) idx (f new_val)

ink

theorem Mt.Utils.List.erase_map_commutes {U : Type u} {V : Type u} (f : U → V) (l : List U) (idx : Nat) : List.map f (List.eraseIdx l idx) = List.eraseIdx (List.map f l) idx