α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
⊢ x ∈ toFinset l
α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x : α
inst✝ : Fintype α
⊢ support (formPerm l) ≤ toFinset l
intro x hx
α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
hx' : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ toFinset l
α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
⊢ x ∈ toFinset l
have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
no goals
α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
hx' : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ toFinset l
simpa using support_formPerm_le' _ hx'
no goals
α : Type u_1
β : Type ?u.746484
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
simpa using hx