case a
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ support (subtypePerm f h) ↔ a✝ ∈ filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
⊢ support (subtypePerm f h) = filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
ext
no goals
case a
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ support (subtypePerm f h) ↔ a✝ ∈ filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
simp [Subtype.ext_iff]