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

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

Tactic:
rw [foldRev_eq, ← Array.foldr_toList, toListModel]

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

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

Tactic:
generalize l.buckets.toList = l

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

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

Tactic:
rw [foldr_cons, ih, AssocList.foldr_apply]

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
induction l generalizing acc with
| nil => simp
| cons x xs ih =>
    rw [foldr_cons, ih, AssocList.foldr_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 γ},
    foldr (fun l acc => AssocList.foldr (fun a b g => f a b :: g) acc l) acc xs =
      map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs) ++ acc
acc : List γ
⊢ map (fun p => f p.fst p.snd) x.toList ++ (map (fun p => f p.fst p.snd) (flatMap AssocList.toList xs) ++ acc) =
    map (fun p => f p.fst p.snd) (flatMap AssocList.toList (x :: xs)) ++ acc

Tactic:
simp

Result:
no goals