case a
α : Type u_1
β : Type ?u.130155
γ : Type ?u.130158
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
α : Type u_1
β : Type ?u.130155
γ : Type ?u.130158
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s
ext x
no goals
case a
α : Type u_1
β : Type ?u.130155
γ : Type ?u.130158
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
simp [@and_comm _ (_ = _), @and_left_comm _ (_ = _), @and_comm (p x) (x ∈ s)]