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

Proof state:
case b
α : 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
⊢ (List.map (fun x => x.toList.length) (source.set i AssocList.nil H).toList).sum +
      (AssocList.foldl reinsertAux target source[i]).size =
    (List.map (fun x => x.toList.length) source.toList).sum + target.size

Tactic:
case b =>
simp only [Array.length_toList, Array.toList_set, Array.get_eq_getElem, AssocList.foldl_eq]
refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_
rw [h₁]
simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList,
  List.length_nil, Nat.sum_append, List.sum_cons, Nat.zero_add, Array.length_toList]
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
(conv => rhs; rw [Nat.add_left_comm]); congr 1
rw [Array.getElem_toList]
have := @reinsertAux_size α β _; simp [Buckets.size] at this
induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl

Result:
no goals

Proof state:
case e_a.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₂
this : ∀ (data : Buckets α β) (a : α) (b : β), (reinsertAux data a b).size = data.size.succ
⊢ (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[i].toList.length + (List.map (fun x => x.toList.length) target.val.toList).sum

Tactic:
simp [Buckets.size] at this

Result:
case e_a.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₂
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
⊢ (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[i].toList.length + (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
⊢ (List.map (fun x => x.toList.length) (source.set i AssocList.nil H).toList).sum +
      (AssocList.foldl reinsertAux target source[i]).size =
    (List.map (fun x => x.toList.length) source.toList).sum + target.size

Tactic:
simp only [Array.length_toList, Array.toList_set, Array.get_eq_getElem, AssocList.foldl_eq]

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
⊢ (List.map (fun x => x.toList.length) (source.toList.set i AssocList.nil)).sum +
      (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).size =
    (List.map (fun x => x.toList.length) source.toList).sum + target.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.set i AssocList.nil H).toList[j]?.getD AssocList.nil = AssocList.nil

Tactic:
simp only [Array.length_toList, Array.toList_set]

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
⊢ (source.toList.set i AssocList.nil)[j]?.getD AssocList.nil = AssocList.nil

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
⊢ (if h : i < source.size then
        let es := source[i];
        let source := source.set i AssocList.nil h;
        let target := AssocList.foldl reinsertAux target es;
        expand.go (i + 1) source target
      else target).size =
    (List.map (fun x => x.toList.length) source.toList).sum + target.size

Tactic:
split

Result:
case isTrue
α : 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
⊢ (let es := source[i];
      let source := source.set i AssocList.nil h✝;
      let target := AssocList.foldl reinsertAux target es;
      expand.go (i + 1) source target).size =
    (List.map (fun x => x.toList.length) source.toList).sum + target.size

case isFalse
α : 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
⊢ target.size = (List.map (fun x => x.toList.length) source.toList).sum + target.size

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 + 0 = buckets.size

Tactic:
simp [Buckets.size]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
⊢ (expand sz buckets).buckets.size = buckets.size

Tactic:
rw [expand, go]

Result:
α : 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

case hs
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
⊢ ∀ (j : Nat), j < 0 → buckets.val.toList[j]?.getD AssocList.nil = AssocList.nil