-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem keys_filterMap [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Option (γ a)} :
    keys (l.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) =
      keys (l.filter fun p => (f p.1 p.2).isSome)

Proof state:
case nil
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) []) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
k : α
v : β k
t : List ((a : α) × β a)
ih :
  keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) t)
⊢ keys
      (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
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t) =
    keys
      (if (f k v).isSome = true then ⟨k, v⟩ :: List.filter (fun p => (f p.fst p.snd).isSome) t
      else List.filter (fun p => (f p.fst p.snd).isSome) t)

Tactic:
cases f k v <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ :
  keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) tail✝) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) tail✝)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (⟨k✝, v✝⟩ :: tail✝)) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) (⟨k✝, v✝⟩ :: tail✝))

Tactic:
next k v t ih =>
simp only [List.filterMap_cons, List.filter_cons]
cases f k v <;> simp [ih]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) l)

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) []) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) [])

case cons
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ :
  keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) tail✝) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) tail✝)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (⟨k✝, v✝⟩ :: tail✝)) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) (⟨k✝, v✝⟩ :: tail✝))

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
k : α
v : β k
t : List ((a : α) × β a)
ih :
  keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) t)
⊢ keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (⟨k, v⟩ :: t)) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) (⟨k, v⟩ :: t))

Tactic:
simp only [List.filterMap_cons, List.filter_cons]

Result:
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
f : (a : α) → β a → Option (γ a)
k : α
v : β k
t : List ((a : α) × β a)
ih :
  keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t) =
    keys (List.filter (fun p => (f p.fst p.snd).isSome) t)
⊢ keys
      (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
      | some b => b :: List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t) =
    keys
      (if (f k v).isSome = true then ⟨k, v⟩ :: List.filter (fun p => (f p.fst p.snd).isSome) t
      else List.filter (fun p => (f p.fst p.snd).isSome) t)