-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem expand_size [Hashable α] {buckets : Buckets α β} :
    (expand sz buckets).buckets.size = buckets.size

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₁).sum + (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    (List.map (fun x => x.toList.length) l₁).sum +
        (source.toList[i].toList.length + (List.map (fun x => x.toList.length) l₂).sum) +
      (List.map (fun x => x.toList.length) target.val.toList).sum

Tactic:
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]

Result:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₁).sum +
      ((List.map (fun x => x.toList.length) l₂).sum +
        (List.map (fun x => x.toList.length)
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum) =
    (List.map (fun x => x.toList.length) l₁).sum +
      (source.toList[i].toList.length +
        ((List.map (fun x => x.toList.length) l₂).sum + (List.map (fun x => x.toList.length) target.val.toList).sum))

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₁).sum +
      ((List.map (fun x => x.toList.length) l₂).sum +
        (List.map (fun x => x.toList.length)
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum) =
    (List.map (fun x => x.toList.length) l₁).sum +
      (source.toList[i].toList.length +
        ((List.map (fun x => x.toList.length) l₂).sum + (List.map (fun x => x.toList.length) target.val.toList).sum))

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    source.toList[i].toList.length +
      ((List.map (fun x => x.toList.length) l₂).sum + (List.map (fun x => x.toList.length) target.val.toList).sum)

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
⊢ (List.map (fun x => x.toList.length) buckets.val.toList).sum + (Buckets.mk (buckets.val.size * 2) ⋯).size =
    buckets.size

Tactic:
rw [Buckets.mk_size]

Result:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
⊢ (List.map (fun x => x.toList.length) buckets.val.toList).sum + 0 = buckets.size

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
j : Nat
hj : j < i + 1
⊢ (source.toList.set i AssocList.nil)[j]?.getD AssocList.nil = AssocList.nil

Tactic:
simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]

Result:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
j : Nat
hj : j < i + 1
⊢ (if i = j then if i < source.size then some AssocList.nil else none else source[j]?).getD AssocList.nil =
    AssocList.nil

Proof state:
case e_a.e_a.cons
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this :
  ∀ (data : Buckets α β) (a : α) (b : β),
    (List.map (fun x => x.toList.length) (reinsertAux data a b).val.toList).sum =
      (List.map (fun x => x.toList.length) data.val.toList).sum + 1
head✝ : α × β
tail✝ : List (α × β)
tail_ih✝ :
  ∀ (target : Buckets α β),
    (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.toList).sum =
      tail✝.length + (List.map (fun x => x.toList.length) target.val.toList).sum
target : Buckets α β
⊢ tail✝.length + ((List.map (fun x => x.toList.length) target.val.toList).sum + 1) =
    tail✝.length + (List.map (fun x => x.toList.length) target.val.toList).sum + 1

Tactic:
rfl

Result:
no goals

Proof state:
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    source.toList[i].toList.length +
      ((List.map (fun x => x.toList.length) l₂).sum + (List.map (fun x => x.toList.length) target.val.toList).sum)

Tactic:
conv => rhs; rw [Nat.add_left_comm]

Result:
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    (List.map (fun x => x.toList.length) l₂).sum +
      (source.toList[i].toList.length + (List.map (fun x => x.toList.length) target.val.toList).sum)