case pos
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l

case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ ↑(formPerm l ^ n) x ∈ l
by_cases h : (l.formPerm ^ n) x = x
no goals
case pos
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l
simpa [h] using hx
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l
have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
rw [← set_support_apply_mem] at h
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x_1 | ↑(formPerm l) x_1 ≠ x_1}
⊢ ↑(formPerm l ^ n) x ∈ l
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
replace h := set_support_zpow_subset _ _ h
no goals
case neg
α : Type u_1
β : Type ?u.825028
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x_1 | ↑(formPerm l) x_1 ≠ x_1}
⊢ ↑(formPerm l ^ n) x ∈ l
simpa using support_formPerm_le' _ h