case h
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
l : List α
h : Subsingleton (Quot.mk Setoid.r l)
⊢ Nodup (Quot.mk Setoid.r l)
α : Type u_1
s : Cycle α
h : Subsingleton s
⊢ Nodup s
induction' s using Quot.inductionOn with l
case h.nil
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
h : Subsingleton (Quot.mk Setoid.r [])
⊢ Nodup (Quot.mk Setoid.r [])

case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
case h
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
l : List α
h : Subsingleton (Quot.mk Setoid.r l)
⊢ Nodup (Quot.mk Setoid.r l)
cases' l with hd tl
no goals
case h.nil
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
h : Subsingleton (Quot.mk Setoid.r [])
⊢ Nodup (Quot.mk Setoid.r [])
simp
case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
have : tl = [] := by simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h
no goals
case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
simp [this]
no goals
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
⊢ tl = []
simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h