These lemmas are used in the internals of HashMap. They should find a new home and/or be reformulated.

theorem List.exists_of_set {α : Type u_1} {i : Nat} {a' : α} {l : List α} (h : i < l.length) : ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l[i] :: l₂ ∧ l₁.length = i ∧ l.set i a' = l₁ ++ a' :: l₂

theorem Array.exists_of_uset {α : Type u_1} (xs : Array α) (i : USize) (d : α) (h : i.toNat < xs.size) : ∃ (l₁ : List α), ∃ (l₂ : List α), xs.toList = l₁ ++ xs[i] :: l₂ ∧ l₁.length = i.toNat ∧ (xs.uset i d h).toList = l₁ ++ d :: l₂