-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
    l.fold (fun acc k v => f k v :: acc) acc =
      ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc

Proof state:
case nil
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : (a : α) → β a → γ
acc : List γ
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc [] =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList []).reverse ++ acc

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
l✝ : Raw α β
acc : List γ
f : (a : α) → β a → γ
l : List (AssocList α β)
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc l =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList l).reverse ++ acc

Tactic:
induction l generalizing acc with
| nil => simp
| cons x xs ih =>
    rw [foldl_cons, ih, AssocList.foldl_apply]
    simp

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : (a : α) → β a → γ
x : AssocList α β
xs : List (AssocList α β)
ih :
  ∀ {acc : List γ},
    foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc xs =
      map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs).reverse ++ acc
acc : List γ
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc (x :: xs) =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList (x :: xs)).reverse ++ acc

Tactic:
rw [foldl_cons, ih, AssocList.foldl_apply]

Result:
case cons
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : (a : α) → β a → γ
x : AssocList α β
xs : List (AssocList α β)
ih :
  ∀ {acc : List γ},
    foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc xs =
      map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs).reverse ++ acc
acc : List γ
⊢ map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs).reverse ++
      ((map (fun p => f p.fst p.snd) x.toList).reverse ++ acc) =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList (x :: xs)).reverse ++ acc

Proof state:
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
acc : List γ
f : (a : α) → β a → γ
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc l.buckets.toList =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList l.buckets.toList).reverse ++ acc

Tactic:
generalize l.buckets.toList = l

Result:
α : Type u
β : α → Type v
γ : Type w
l✝ : Raw α β
acc : List γ
f : (a : α) → β a → γ
l : List (AssocList α β)
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc l =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList l).reverse ++ acc

Proof state:
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
acc : List γ
f : (a : α) → β a → γ
⊢ Raw.fold (fun acc k v => f k v :: acc) acc l = map (fun p => f p.fst p.snd) (toListModel l.buckets).reverse ++ acc

Tactic:
rw [fold_eq, ← Array.foldl_toList, toListModel]

Result:
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
acc : List γ
f : (a : α) → β a → γ
⊢ foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc l.buckets.toList =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList l.buckets.toList).reverse ++ acc

Proof state:
case cons
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : (a : α) → β a → γ
x : AssocList α β
xs : List (AssocList α β)
ih :
  ∀ {acc : List γ},
    foldl (fun acc l => AssocList.foldl (fun acc k v => f k v :: acc) acc l) acc xs =
      map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs).reverse ++ acc
acc : List γ
⊢ map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs).reverse ++
      ((map (fun p => f p.fst p.snd) x.toList).reverse ++ acc) =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList (x :: xs)).reverse ++ acc

Tactic:
simp

Result:
no goals