-- 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 [] ++ g []).length
⊢ (g []).length = 0

Tactic:
rw [List.length_append, List.append_nil] at this

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 []).length + (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 : 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))

Tactic:
apply ih

Result:
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)

Proof state:
case cons
α : 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 [] = []
head✝ : AssocList α β
tail✝ : List (AssocList α β)
tail_ih✝ :
  ∀ (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' tail✝).Perm
        (g (List.foldl (fun acc a => acc ++ a.toList) l'' tail✝))
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' (head✝ :: tail✝)).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) l'' (head✝ :: tail✝)))

Tactic:
next l t ih =>
simp only [List.foldl_cons]
apply ih
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')
⊢ (toListModel (updateAllBuckets m.val.buckets f)).Perm (g (toListModel m.val.buckets))

Tactic:
have hg₀ : g [] = [] := by
  rw [← List.length_eq_zero]
  have := (hg (l := []) (l' := [])).length_eq
  rw [List.length_append, List.append_nil] at this
  omega

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 [] = []
⊢ (toListModel (updateAllBuckets m.val.buckets f)).Perm (g (toListModel m.val.buckets))

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

Tactic:
induction l generalizing l' l''

Result:
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'' []))

case cons
α : 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 [] = []
head✝ : AssocList α β
tail✝ : List (AssocList α β)
tail_ih✝ :
  ∀ (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' tail✝).Perm
        (g (List.foldl (fun acc a => acc ++ a.toList) l'' tail✝))
l' : List ((a : α) × δ a)
l'' : List ((a : α) × β a)
h : (g l'').Perm l'
⊢ (List.foldl (fun acc a => acc ++ (f a).toList) l' (head✝ :: tail✝)).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) l'' (head✝ :: tail✝)))

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

Tactic:
simpa using this m.1.buckets.toList [] [] (by 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')
⊢ g [] = []

Tactic:
rw [← List.length_eq_zero]

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')
⊢ (g []).length = 0