-- 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₁ ++ 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

Tactic:
rw [h₁]

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) (l₁ ++ source.toList[i] :: l₂)).sum + target.size

Proof state:
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

Tactic:
nofun

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 =
    (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)

Tactic:
congr 1

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.toList[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
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) (l₁ ++ source.toList[i] :: l₂)).sum + target.size

Tactic:
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]

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

Tactic:
refine List.ext_getElem (by simp) fun j h₁ h₂ => ?_

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
⊢ (List.map (fun x => AssocList.nil) source.toList)[j] = source.toList[j]

Proof state:
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

Tactic:
cases source.toList[j]? <;> rfl

Result:
no goals

Proof state:
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

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

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
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]

Tactic:
rwa [List.getElem?_eq_getElem] at this

Result:
no goals