α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filterMap (Option.guard fun x => decide (p x) = true) l
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filter (fun b => decide (p b)) l
rw [← List.filterMap_eq_filter]
case e_f
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ Option.guard p = Option.guard fun x => decide (p x) = true
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filterMap (Option.guard fun x => decide (p x) = true) l
congr
case e_f.h
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
a : α
⊢ Option.guard p a = Option.guard (fun x => decide (p x) = true) a
case e_f
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ Option.guard p = Option.guard fun x => decide (p x) = true
funext a
no goals
case e_f.h
α : Type u_1
β : Type ?u.277023
γ : Type ?u.277026
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
a : α
⊢ Option.guard p a = Option.guard (fun x => decide (p x) = true) a
simp