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

Tactic:
next h => exact (ih _).trans (by simp [h])

Result:
no goals

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)
h : f k v = none
⊢ (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)

Tactic:
simp [h]

Result:
no goals

Proof state:
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)

Tactic:
next h =>
refine (ih _).trans ?_
simp only [toList_cons, List.cons_append]
exact perm_middle.symm.trans (by simp [h])

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
f : (a : α) → β a → Option (γ a)
l : AssocList α β
this :
  ∀ (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)
⊢ (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)

Tactic:
simpa using this .nil l

Result:
no goals

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

Tactic:
simp only [toList_cons, List.cons_append]

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✝
⊢ (⟨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:
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)

Tactic:
simp [filterMap.go]

Result:
no goals

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:
intros l l'

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

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

Tactic:
exact (ih _).trans (by simp [h])

Result:
no goals

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

Tactic:
exact perm_middle.symm.trans (by simp [h])

Result:
no goals