-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem computeSize_eq {buckets : Array (AssocList α β)} :
    computeSize buckets = (toListModel buckets).length

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
⊢ computeSize buckets = (toListModel buckets).length

Tactic:
rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_toList]

Result:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
⊢ Array.foldl (fun d b => d + b.length) 0 buckets = (Array.foldl (fun acc a => acc ++ a.toList) [] buckets).length

Proof state:
case nil
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length [] = (foldl (fun acc a => acc ++ a.toList) l' []).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
⊢ Array.foldl (fun d b => d + b.length) 0 buckets = (Array.foldl (fun acc a => acc ++ a.toList) [] buckets).length

Tactic:
suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
    l.foldl (fun d b => d + b.toList.length) l'.length =
      (l.foldl (fun acc a => acc ++ a.toList) l').length
  by simpa using this buckets.toList []

Result:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
⊢ ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length l = (foldl (fun acc a => acc ++ a.toList) l' l).length

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
this :
  ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length l = (foldl (fun acc a => acc ++ a.toList) l' l).length
⊢ Array.foldl (fun d b => d + b.length) 0 buckets = (Array.foldl (fun acc a => acc ++ a.toList) [] buckets).length

Tactic:
simpa using this buckets.toList []

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
head✝ : AssocList α β
tail✝ : List (AssocList α β)
tail_ih✝ :
  ∀ (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length tail✝ = (foldl (fun acc a => acc ++ a.toList) l' tail✝).length
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length (head✝ :: tail✝) =
    (foldl (fun acc a => acc ++ a.toList) l' (head✝ :: tail✝)).length

Tactic:
next l₂ t ih => rw [foldl_cons, ← List.length_append, ih, foldl_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
l₂ : AssocList α β
t : List (AssocList α β)
ih :
  ∀ (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length t = (foldl (fun acc a => acc ++ a.toList) l' t).length
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length (l₂ :: t) =
    (foldl (fun acc a => acc ++ a.toList) l' (l₂ :: t)).length

Tactic:
rw [foldl_cons, ← List.length_append, ih, foldl_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
l : List (AssocList α β)
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length l = (foldl (fun acc a => acc ++ a.toList) l' l).length

Tactic:
induction l generalizing l'

Result:
case nil
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length [] = (foldl (fun acc a => acc ++ a.toList) l' []).length

case cons
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
head✝ : AssocList α β
tail✝ : List (AssocList α β)
tail_ih✝ :
  ∀ (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length tail✝ = (foldl (fun acc a => acc ++ a.toList) l' tail✝).length
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length (head✝ :: tail✝) =
    (foldl (fun acc a => acc ++ a.toList) l' (head✝ :: tail✝)).length

Proof state:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
⊢ ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
    foldl (fun d b => d + b.toList.length) l'.length l = (foldl (fun acc a => acc ++ a.toList) l' l).length

Tactic:
intro l l'

Result:
α : Type u
β : α → Type v
buckets : Array (AssocList α β)
l : List (AssocList α β)
l' : List ((a : α) × β a)
⊢ foldl (fun d b => d + b.toList.length) l'.length l = (foldl (fun acc a => acc ++ a.toList) l' l).length