α : Type u_1
s : Cycle α
h : Nodup s
⊢ Nontrivial s ↔ ¬length s ≤ 1
α : Type u_1
s : Cycle α
h : Nodup s
⊢ Nontrivial s ↔ ¬Subsingleton s
rw [length_subsingleton_iff]
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
α : Type u_1
s : Cycle α
h : Nodup s
⊢ Nontrivial s ↔ ¬length s ≤ 1
induction s using Quotient.inductionOn'
case h
α : Type u_1
a✝ : List α
h : List.Nodup a✝
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
simp only [mk''_eq_coe, nodup_coe_iff] at h
no goals
case h
α : Type u_1
a✝ : List α
h : List.Nodup a✝
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
simp [h, Nat.succ_le_iff]