-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_map {f : (a : α) → β a → γ a} {l : AssocList α β} :
    Perm (l.map f).toList (l.toList.map fun p => ⟨p.1, f p.1 p.2⟩)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
this :
  ∀ (l : AssocList α γ) (l' : AssocList α β),
    (map.go f l l').toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'.toList)
⊢ (map.go f nil l).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList)

Tactic:
simpa using this .nil l

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
⊢ ∀ (l : AssocList α γ) (l' : AssocList α β),
    (map.go f l l').toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'.toList)

Tactic:
intros l l'

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
l : AssocList α γ
l' : AssocList α β
⊢ (map.go f l l').toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'.toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α γ), (map.go f l t).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)
l : AssocList α γ
⊢ (map.go f l (cons k v t)).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (cons k v t).toList)

Tactic:
simp only [map.go, toList_cons, List.map_cons]

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α γ), (map.go f l t).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)
l : AssocList α γ
⊢ (map.go f (cons k (f k v) l) t).toList.Perm
    (l.toList ++ ⟨k, f k v⟩ :: List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
l : AssocList α γ
l' : AssocList α β
⊢ (map.go f l l').toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'.toList)

Tactic:
induction l' generalizing l

Result:
case nil
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
l : AssocList α γ
⊢ (map.go f l nil).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) nil.toList)

case cons
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ :
  ∀ (l : AssocList α γ),
    (map.go f l tail✝).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) tail✝.toList)
l : AssocList α γ
⊢ (map.go f l (cons key✝ value✝ tail✝)).toList.Perm
    (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (cons key✝ value✝ tail✝).toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α γ), (map.go f l t).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)
l : AssocList α γ
⊢ ((cons k (f k v) l).toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList).Perm
    (l.toList ++ ⟨k, f k v⟩ :: List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)

Tactic:
simpa using perm_middle.symm

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
l : AssocList α γ
⊢ (map.go f l nil).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) nil.toList)

Tactic:
simp [map.go]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ :
  ∀ (l : AssocList α γ),
    (map.go f l tail✝).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) tail✝.toList)
l : AssocList α γ
⊢ (map.go f l (cons key✝ value✝ tail✝)).toList.Perm
    (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (cons key✝ value✝ tail✝).toList)

Tactic:
next k v t ih =>
simp only [map.go, toList_cons, List.map_cons]
refine (ih _).trans ?_
simpa using perm_middle.symm

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
⊢ (map f l).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList)

Tactic:
rw [map]

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
⊢ (map.go f nil l).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α γ), (map.go f l t).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)
l : AssocList α γ
⊢ (map.go f (cons k (f k v) l) t).toList.Perm
    (l.toList ++ ⟨k, f k v⟩ :: List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)

Tactic:
refine (ih _).trans ?_

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α γ), (map.go f l t).toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)
l : AssocList α γ
⊢ ((cons k (f k v) l).toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList).Perm
    (l.toList ++ ⟨k, f k v⟩ :: List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
⊢ (map.go f nil l).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList)

Tactic:
suffices ∀ l l', Perm (map.go f l l').toList
    (l.toList ++ l'.toList.map fun p => ⟨p.1, f p.1 p.2⟩) by
  simpa using this .nil l

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → γ a
l : AssocList α β
⊢ ∀ (l : AssocList α γ) (l' : AssocList α β),
    (map.go f l l').toList.Perm (l.toList ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'.toList)