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

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

Tactic:
simp only [filterMap.go, toList_cons, List.filterMap_cons]

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih :
  ∀ (l : AssocList α γ),
    (filterMap.go f l t).toList.Perm
      (l.toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)
l : AssocList α γ
⊢ (match f k v with
        | none => filterMap.go f l t
        | some v' => filterMap.go f (cons k v' l) t).toList.Perm
    (l.toList ++
      match Option.map (fun x => ⟨k, x⟩) (f k v) with
      | none => List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)

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

Tactic:
refine (ih _).trans ?_

Result:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih :
  ∀ (l : AssocList α γ),
    (filterMap.go f l t).toList.Perm
      (l.toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)
l : AssocList α γ
x✝ : Option (γ k)
b✝ : γ k
h : f k v = some b✝
⊢ ((cons k b✝ l).toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList).Perm
    (l.toList ++
      match Option.map (fun x => ⟨k, x⟩) (f k v) with
      | none => List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih :
  ∀ (l : AssocList α γ),
    (filterMap.go f l t).toList.Perm
      (l.toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)
l : AssocList α γ
x✝ : Option (γ k)
b✝ : γ k
h : f k v = some b✝
⊢ (l.toList ++ ⟨k, b✝⟩ :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList).Perm
    (l.toList ++
      match Option.map (fun x => ⟨k, x⟩) (f k v) with
      | none => List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)

Tactic:
simp [h]

Result:
no goals

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

Tactic:
rw [filterMap]

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

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

Tactic:
induction l' generalizing l

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

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

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

Tactic:
split

Result:
case h_1
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih :
  ∀ (l : AssocList α γ),
    (filterMap.go f l t).toList.Perm
      (l.toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)
l : AssocList α γ
x✝ : Option (γ k)
heq✝ : f k v = none
⊢ (filterMap.go f l t).toList.Perm
    (l.toList ++
      match Option.map (fun x => ⟨k, x⟩) (f k v) with
      | none => List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)

case h_2
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l✝ : AssocList α β
k : α
v : β k
t : AssocList α β
ih :
  ∀ (l : AssocList α γ),
    (filterMap.go f l t).toList.Perm
      (l.toList ++ List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)
l : AssocList α γ
x✝ : Option (γ k)
b✝ : γ k
heq✝ : f k v = some b✝
⊢ (filterMap.go f (cons k b✝ l) t).toList.Perm
    (l.toList ++
      match Option.map (fun x => ⟨k, x⟩) (f k v) with
      | none => List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList)