-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem reinsertAux_size [Hashable α] (data : Buckets α β) (a : α) (b : β) :
    (reinsertAux data a b).size = data.size.succ

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
⊢ (reinsertAux data a b).size = data.size.succ

Tactic:
simp only [reinsertAux, Array.length_toList, Array.ugetElem_eq_getElem, Buckets.size_eq,
  Nat.succ_eq_add_one]

Result:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
⊢ (List.map (fun x => x.toList.length)
        (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
              ⋯).val.toList).sum =
    (List.map (fun x => x.toList.length) data.val.toList).sum + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.toList = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂
left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat
eq :
  (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
          ⋯).val.toList =
    l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂
⊢ (List.map (fun x => x.toList.length)
        (l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂)).sum =
    (List.map (fun x => x.toList.length) data.val.toList).sum + 1

Tactic:
simp [h₁, Nat.succ_add]

Result:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.toList = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂
left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat
eq :
  (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
          ⋯).val.toList =
    l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂
⊢ (List.map (fun x => x.toList.length) l₁).sum +
      (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + (List.map (fun x => x.toList.length) l₂).sum +
        1) =
    (List.map (fun x => x.toList.length) l₁).sum +
        (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + (List.map (fun x => x.toList.length) l₂).sum) +
      1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
⊢ (List.map (fun x => x.toList.length)
        (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
              ⋯).val.toList).sum =
    (List.map (fun x => x.toList.length) data.val.toList).sum + 1

Tactic:
refine have ⟨l₁, l₂, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_

Result:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.toList = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂
left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat
eq :
  (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
          ⋯).val.toList =
    l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂
⊢ (List.map (fun x => x.toList.length)
        (l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂)).sum =
    (List.map (fun x => x.toList.length) data.val.toList).sum + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Hashable α
data : Buckets α β
a : α
b : β
l₁ l₂ : List (AssocList α β)
h₁ : data.val.toList = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂
left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat
eq :
  (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat])
          ⋯).val.toList =
    l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂
⊢ (List.map (fun x => x.toList.length) l₁).sum +
      (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + (List.map (fun x => x.toList.length) l₂).sum +
        1) =
    (List.map (fun x => x.toList.length) l₁).sum +
        (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + (List.map (fun x => x.toList.length) l₂).sum) +
      1

Tactic:
rfl

Result:
no goals