α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
              (AssocList.cons a b
                data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
              (_ :
                USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
                  Array.size data.val)).val.data) =
    Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
⊢ Bucket.size (reinsertAux data a b) = Nat.succ (Bucket.size data)
simp [Bucket.size_eq, reinsertAux]
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.data = l₁ ++ data.val[(mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
left✝ : List.length l₁ = USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
eq :
  (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
          (AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
              Array.size data.val)).val.data =
    l₁ ++
      AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (l₁ ++
          AssocList.cons a b
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] ::
            l₂)) =
    Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
              (AssocList.cons a b
                data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
              (_ :
                USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
                  Array.size data.val)).val.data) =
    Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
refine have ⟨l₁, l₂, h₁, _, eq⟩ := Bucket.exists_of_update ..; eq ▸ ?_
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.data = l₁ ++ data.val[(mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
left✝ : List.length l₁ = USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
eq :
  (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
          (AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
              Array.size data.val)).val.data =
    l₁ ++
      AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      Nat.succ
        (List.length
            (AssocList.toList
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val]) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)) =
    Nat.succ
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        (List.length
            (AssocList.toList
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val]) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)))
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.data = l₁ ++ data.val[(mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
left✝ : List.length l₁ = USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
eq :
  (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
          (AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
              Array.size data.val)).val.data =
    l₁ ++
      AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (l₁ ++
          AssocList.cons a b
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] ::
            l₂)) =
    Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
simp [h₁, Nat.succ_add]
no goals
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Bucket α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.data = l₁ ++ data.val[(mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
left✝ : List.length l₁ = USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
eq :
  (Bucket.update data (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val
          (AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val <
              Array.size data.val)).val.data =
    l₁ ++
      AssocList.cons a b data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val] :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      Nat.succ
        (List.length
            (AssocList.toList
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val]) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)) =
    Nat.succ
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        (List.length
            (AssocList.toList
              data.val[USize.toNat (mkIdx (_ : 0 < Array.size data.val) (UInt64.toUSize (hash a))).val]) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)))
rfl