α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d : AssocList α β
h : USize.toNat i < Array.size self.val
⊢ ∃ l₁ l₂,
    self.val.data = l₁ ++ List.get self.val.data { val := USize.toNat i, isLt := h } :: l₂ ∧
      List.length l₁ = USize.toNat i ∧ (update self i d h).val.data = l₁ ++ d :: l₂
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d : AssocList α β
h : USize.toNat i < Array.size self.val
⊢ ∃ l₁ l₂,
    self.val.data = l₁ ++ self.val[i] :: l₂ ∧
      List.length l₁ = USize.toNat i ∧ (update self i d h).val.data = l₁ ++ d :: l₂
simp [Array.getElem_eq_data_get]
no goals
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d : AssocList α β
h : USize.toNat i < Array.size self.val
⊢ ∃ l₁ l₂,
    self.val.data = l₁ ++ List.get self.val.data { val := USize.toNat i, isLt := h } :: l₂ ∧
      List.length l₁ = USize.toNat i ∧ (update self i d h).val.data = l₁ ++ d :: l₂
exact List.exists_of_set' h