-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β → AssocList α δ}
    {g : List ((a : α) × β a) → List ((a : α) × δ a)}
    (hfg : ∀ {l}, Perm ((f l).toList) (g l.toList))
    (hg : ∀ {l l'}, Perm (g (l ++ l')) (g l ++ g l')) :
    Perm (toListModel (updateAllBuckets m.1.buckets f)) (g (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
this : (g []).length = (g []).length + (g []).length
⊢ (g []).length = 0

Tactic:
omega

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' []).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' []))

Tactic:
simpa using h.symm

Result:
no goals

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
l : AssocList α β
t : List (AssocList α β)
ih :
  ∀ (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' t).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' t))
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' (l :: t)).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) l'' (l :: t)))

Tactic:
simp only [List.foldl_cons]

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
l : AssocList α β
t : List (AssocList α β)
ih :
  ∀ (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' t).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' t))
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) (l' ++ (f l).toList) t).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) (l'' ++ l.toList) t))

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
⊢ (g []).length = 0

Tactic:
have := (hg (l := []) (l' := [])).length_eq

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
this : (g ([] ++ [])).length = (g [] ++ g []).length
⊢ (g []).length = 0

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
⊢ ∀ (l : List (AssocList α β)) (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' l).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' l))

Tactic:
rintro l l' l'' h

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
l : List (AssocList α β)
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' l).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' l))

Proof state:
case h
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
l : AssocList α β
t : List (AssocList α β)
ih :
  ∀ (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' t).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' t))
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (g (l'' ++ l.toList)).Perm (l' ++ (f l).toList)

Tactic:
exact hg.trans (Perm.append h hfg.symm)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
this :
  ∀ (l : List (AssocList α β)) (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' l).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' l))
⊢ (g []).Perm []

Tactic:
simp [hg₀]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
⊢ (toListModel (updateAllBuckets m.val.buckets f)).Perm (g (toListModel m.val.buckets))

Tactic:
rw [updateAllBuckets, toListModel, Array.toList_map, List.flatMap_eq_foldl, List.foldl_map,
  toListModel, List.flatMap_eq_foldl]

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
⊢ (List.foldl (fun x y => x ++ (f y).toList) [] m.val.buckets.toList).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) [] m.val.buckets.toList))