case H
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
⊢ ↑(formPerm l ^ length l) x = ↑1 x
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
⊢ formPerm l ^ length l = 1
ext x
case pos
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x

case neg
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x
case H
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
⊢ ↑(formPerm l ^ length l) x = ↑1 x
by_cases hx : x ∈ l
case pos.intro.intro
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l ^ length l) (nthLe l k hk) = ↑1 (nthLe l k hk)
case pos
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
no goals
case pos.intro.intro
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l ^ length l) (nthLe l k hk) = ↑1 (nthLe l k hk)
simp [formPerm_pow_apply_nthLe _ hl, Nat.mod_eq_of_lt hk]
case neg
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
this : ¬x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ ↑(formPerm l ^ length l) x = ↑1 x
case neg
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x
have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
  intro H
  refine' hx _
  replace H := set_support_zpow_subset l.formPerm l.length H
  simpa using support_formPerm_le' _ H
no goals
case neg
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
this : ¬x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ ↑(formPerm l ^ length l) x = ↑1 x
simpa using this
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ False
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
⊢ ¬x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
intro H
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ x ∈ l
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ False
refine' hx _
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ l
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ x ∈ l
replace H := set_support_zpow_subset l.formPerm l.length H
no goals
α : Type u_1
β : Type ?u.842481
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ l
simpa using support_formPerm_le' _ H