α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d d' : AssocList α β
h : USize.toNat i < Array.size self.val
h' : USize.toNat i < Array.size (update self i d h).val
⊢ { val := Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' } d',
      property :=
        (_ :
          (fun b => 0 < Array.size b)
            (Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' }
              d')) } =
    { val := Array.set self.val { val := USize.toNat i, isLt := h } d',
      property := (_ : (fun b => 0 < Array.size b) (Array.set self.val { val := USize.toNat i, isLt := h } d')) }
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d d' : AssocList α β
h : USize.toNat i < Array.size self.val
h' : USize.toNat i < Array.size (update self i d h).val
⊢ update (update self i d h) i d' h' = update self i d' h
simp [update]
case e_val
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d d' : AssocList α β
h : USize.toNat i < Array.size self.val
h' : USize.toNat i < Array.size (update self i d h).val
⊢ Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' } d' =
    Array.set self.val { val := USize.toNat i, isLt := h } d'
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d d' : AssocList α β
h : USize.toNat i < Array.size self.val
h' : USize.toNat i < Array.size (update self i d h).val
⊢ { val := Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' } d',
      property :=
        (_ :
          (fun b => 0 < Array.size b)
            (Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' }
              d')) } =
    { val := Array.set self.val { val := USize.toNat i, isLt := h } d',
      property := (_ : (fun b => 0 < Array.size b) (Array.set self.val { val := USize.toNat i, isLt := h } d')) }
congr 1
no goals
case e_val
α : Type u_1
β : Type u_2
self : Bucket α β
i : USize
d d' : AssocList α β
h : USize.toNat i < Array.size self.val
h' : USize.toNat i < Array.size (update self i d h).val
⊢ Array.set (Array.set self.val { val := USize.toNat i, isLt := h } d) { val := USize.toNat i, isLt := h' } d' =
    Array.set self.val { val := USize.toNat i, isLt := h } d'
rw [Array.set_set]