case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ formPerm (Quot.mk Setoid.r s) (_ : Nodup (Quot.mk Setoid.r s)) = 1
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Subsingleton s
⊢ formPerm s (_ : Nodup s) = 1
induction' s using Quot.inductionOn with s
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ List.formPerm s = 1
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ formPerm (Quot.mk Setoid.r s) (_ : Nodup (Quot.mk Setoid.r s)) = 1
simp only [formPerm_coe, mk_eq_coe]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : List.length s ≤ 1
⊢ List.formPerm s = 1
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ List.formPerm s = 1
simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h
case h.nil
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
h : List.length [] ≤ 1
⊢ List.formPerm [] = 1

case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : List.length (hd :: tl) ≤ 1
⊢ List.formPerm (hd :: tl) = 1
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : List.length s ≤ 1
⊢ List.formPerm s = 1
cases' s with hd tl
no goals
case h.nil
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
h : List.length [] ≤ 1
⊢ List.formPerm [] = 1
simp
case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : tl = []
⊢ List.formPerm (hd :: tl) = 1
case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : List.length (hd :: tl) ≤ 1
⊢ List.formPerm (hd :: tl) = 1
simp only [length_eq_zero, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h
no goals
case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : tl = []
⊢ List.formPerm (hd :: tl) = 1
simp [h]