α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
⊢ x ∈ {y | ↑(formPerm l) y ≠ y}
α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
⊢ x ∈ l
suffices x ∈ { y | formPerm l y ≠ y } by
  rw [← mem_toFinset]
  exact support_formPerm_le' _ this
no goals
α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
⊢ x ∈ {y | ↑(formPerm l) y ≠ y}
simpa using h
α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
this : x ∈ {y | ↑(formPerm l) y ≠ y}
⊢ x ∈ toFinset l
α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
this : x ∈ {y | ↑(formPerm l) y ≠ y}
⊢ x ∈ l
rw [← mem_toFinset]
no goals
α : Type u_1
β : Type ?u.815968
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
this : x ∈ {y | ↑(formPerm l) y ≠ y}
⊢ x ∈ toFinset l
exact support_formPerm_le' _ this