α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) =
    map Sigma.fst (eraseP ((fun b => decide (a = b)) ∘ Sigma.fst) l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ keys (kerase a l) = List.erase (keys l) a
rw [keys, kerase, erase_eq_eraseP, eraseP_map]
no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) =
    map Sigma.fst (eraseP ((fun b => decide (a = b)) ∘ Sigma.fst) l)
dsimp [Function.comp]