α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ m.size =
    Bucket.size
      (Bucket.update
        (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val AssocList.nil
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
              Array.size m.buckets.val))
        (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
        (AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size
              (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                  AssocList.nil
                  (_ :
                    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                      Array.size m.buckets.val)).val))
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ (modify m k f).size = Bucket.size (modify m k f).buckets
dsimp [modify, cond]
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ m.size =
    Bucket.size
      (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
        (AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size m.buckets.val))
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ m.size =
    Bucket.size
      (Bucket.update
        (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val AssocList.nil
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
              Array.size m.buckets.val))
        (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
        (AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size
              (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                  AssocList.nil
                  (_ :
                    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                      Array.size m.buckets.val)).val))
rw [Bucket.update_update]
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.modify k f
                m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
              (_ :
                USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                  Array.size m.buckets.val)).val.data)
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ m.size =
    Bucket.size
      (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
        (AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size m.buckets.val))
simp [h, Bucket.size]
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
w✝¹ w✝ : List (AssocList α β)
h₁ :
  m.buckets.val.data =
    w✝¹ ++ m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] :: w✝
left✝ : List.length w✝¹ = USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
eq :
  (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
          (AssocList.modify k f
            m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
              Array.size m.buckets.val)).val.data =
    w✝¹ ++
      AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ::
        w✝
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (w✝¹ ++
          AssocList.modify k f
              m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ::
            w✝))
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.modify k f
                m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
              (_ :
                USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                  Array.size m.buckets.val)).val.data)
refine have ⟨_, _, h₁, _, eq⟩ := Bucket.exists_of_update ..; eq ▸ ?_
no goals
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = Bucket.size m.buckets
w✝¹ w✝ : List (AssocList α β)
h₁ :
  m.buckets.val.data =
    w✝¹ ++ m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] :: w✝
left✝ : List.length w✝¹ = USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
eq :
  (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
          (AssocList.modify k f
            m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
          (_ :
            USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
              Array.size m.buckets.val)).val.data =
    w✝¹ ++
      AssocList.modify k f
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ::
        w✝
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) m.buckets.val.data) =
    Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (w✝¹ ++
          AssocList.modify k f
              m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ::
            w✝))
simp [h, h₁, Bucket.size_eq]