-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} :
    Perm (l.filter f).toList (l.toList.filter fun p => f p.1 p.2)

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

Tactic:
intros l l'

Result:
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ l l' : AssocList α β
⊢ (filter.go f l l').toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) l'.toList)

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

Tactic:
simpa using this .nil l

Result:
no goals

Proof state:
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l : AssocList α β
⊢ (filter f l).toList.Perm (List.filter (fun p => f p.fst p.snd) l.toList)

Tactic:
rw [filter]

Result:
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l : AssocList α β
⊢ (filter.go f nil l).toList.Perm (List.filter (fun p => f p.fst p.snd) l.toList)

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

Tactic:
exact (ih _).trans (by simpa using perm_middle.symm)

Result:
no goals

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

Tactic:
simpa using perm_middle.symm

Result:
no goals

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

Tactic:
split

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

case isFalse
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α β), (filter.go f l t).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) t.toList)
l : AssocList α β
h✝ : ¬f k v = true
⊢ (filter.go f l t).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) t.toList)

Proof state:
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ l l' : AssocList α β
⊢ (filter.go f l l').toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) l'.toList)

Tactic:
induction l' generalizing l

Result:
case nil
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ l : AssocList α β
⊢ (filter.go f l nil).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) nil.toList)

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

Proof state:
case isFalse
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih : ∀ (l : AssocList α β), (filter.go f l t).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) t.toList)
l : AssocList α β
h✝ : ¬f k v = true
⊢ (filter.go f l t).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) t.toList)

Tactic:
exact ih _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l : AssocList α β
⊢ (filter.go f nil l).toList.Perm (List.filter (fun p => f p.fst p.snd) l.toList)

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

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

Proof state:
case nil
α : Type u
β : α → Type v
f : (a : α) → β a → Bool
l✝ l : AssocList α β
⊢ (filter.go f l nil).toList.Perm (l.toList ++ List.filter (fun p => f p.fst p.snd) nil.toList)

Tactic:
simp [filter.go]

Result:
no goals

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

Tactic:
simp only [filter.go, toList_cons, List.filter_cons, cond_eq_if]

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