-- 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
⊢ (expand.go i source target).size = (List.map (fun x => x.toList.length) source.toList).sum + target.size

Tactic:
unfold expand.go

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

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
⊢ (if i = j then if i < source.size then some AssocList.nil else none else source[j]?).getD AssocList.nil =
    AssocList.nil

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
j : Nat
hj : j < i + 1
h✝ : i = j
⊢ (some AssocList.nil).getD AssocList.nil = AssocList.nil

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
j : Nat
hj : j < i + 1
h✝ : ¬i = j
⊢ source[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
H : ¬i < source.size
⊢ (List.map ((fun x => x.toList.length) ∘ fun x => AssocList.nil) source.toList).sum = 0

Tactic:
induction source.toList <;> simp [*]

Result:
no goals

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) (List.map (fun x => AssocList.nil) source.toList)).sum = 0

Tactic:
simp only [List.map_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
⊢ (List.map ((fun x => x.toList.length) ∘ fun x => AssocList.nil) source.toList).sum = 0

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 => AssocList.nil) source.toList).length = source.toList.length

Tactic:
simp

Result:
no goals

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
H : ¬i = j
⊢ source[j]?.getD AssocList.nil = AssocList.nil

Tactic:
exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))

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₂
⊢ (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) target.val.toList).sum

Tactic:
rw [Array.getElem_toList]

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₂
⊢ (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.toList).sum = 0

Tactic:
rw [← (_ : source.toList.map (fun _ => .nil) = source.toList)]

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) (List.map (fun x => AssocList.nil) source.toList)).sum = 0

α : 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 => AssocList.nil) source.toList = source.toList

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

Tactic:
rw [(_ : List.sum _ = 0), Nat.zero_add]

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).sum = 0