case mk.mk
α : Type u_1
β : Type ?u.50561
γ : Type ?u.50564
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs } ↔
    ∀ {x : α}, ↑f x ≠ x → x ∈ { val := Quot.mk Setoid.r l, nodup := hs }
α : Type u_1
β : Type ?u.50561
γ : Type ?u.50564
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, ↑f x ≠ x → x ∈ s
rintro ⟨⟨l⟩, hs⟩ f
no goals
case mk.mk
α : Type u_1
β : Type ?u.50561
γ : Type ?u.50564
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs } ↔
    ∀ {x : α}, ↑f x ≠ x → x ∈ { val := Quot.mk Setoid.r l, nodup := hs }
exact mem_permsOfList_iff