-- 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
⊢ (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

Tactic:
refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; 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
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₁ ++ AssocList.nil :: l₂)).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
h₁ : j < (List.map (fun x => AssocList.nil) source.toList).length
h₂ : j < source.toList.length
⊢ AssocList.nil = source.toList[j]

Tactic:
have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm

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
h₁ : j < (List.map (fun x => AssocList.nil) source.toList).length
h₂ : j < source.toList.length
this : AssocList.nil = source.toList[j]?.getD AssocList.nil
⊢ AssocList.nil = source.toList[j]

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 : β),
    (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

Tactic:
induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]

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

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₂
⊢ (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:
have := @reinsertAux_size α β _

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 : β), (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

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
⊢ (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

Tactic:
refine (go (i+1) _ _ fun j hj => ?a).trans ?b

Result:
case 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
j : Nat
hj : j < i + 1
⊢ (source.set i AssocList.nil H).toList[j]?.getD AssocList.nil = AssocList.nil

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