case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ ↑(formPerm (Quot.mk Setoid.r a✝) h) x = next (Quot.mk Setoid.r a✝) h x hx
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
x : α
hx : x ∈ s
⊢ ↑(formPerm s h) x = next s h x hx
induction s using Quot.inductionOn
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ ↑(formPerm (Quot.mk Setoid.r a✝) h) x = next (Quot.mk Setoid.r a✝) h x hx
simpa using List.formPerm_apply_mem_eq_next h _ (by simp_all)
no goals
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ x ∈ a✝
simp_all