case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ support (formPerm (Quot.mk Setoid.r s) h) = toFinset (Quot.mk Setoid.r s)
α : Type u_1
inst✝¹ : DecidableEq α
s✝ s' : Cycle α
inst✝ : Fintype α
s : Cycle α
h : Nodup s
hn : Nontrivial s
⊢ support (formPerm s h) = toFinset s
induction' s using Quot.inductionOn with s
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ ∀ (x : α), s ≠ [x]
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ support (formPerm (Quot.mk Setoid.r s) h) = toFinset (Quot.mk Setoid.r s)
refine' support_formPerm_of_nodup s h _
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝ s' : Cycle α
inst✝ : Fintype α
s : Cycle α
h✝ : Nodup s
hn✝ : Nontrivial s
x✝ : α
h : Nodup (Quot.mk Setoid.r [x✝])
hn : Nontrivial (Quot.mk Setoid.r [x✝])
⊢ False
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ ∀ (x : α), s ≠ [x]
rintro _ rfl
no goals
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝ s' : Cycle α
inst✝ : Fintype α
s : Cycle α
h✝ : Nodup s
hn✝ : Nontrivial s
x✝ : α
h : Nodup (Quot.mk Setoid.r [x✝])
hn : Nontrivial (Quot.mk Setoid.r [x✝])
⊢ False
simpa [Nat.succ_le_succ_iff] using length_nontrivial hn