case intro.intro.intro.intro
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ length s
α : Type u_1
s : Cycle α
h : Nontrivial s
⊢ 2 ≤ length s
obtain ⟨x, y, hxy, hx, hy⟩ := h
case intro.intro.intro.intro.h
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
hy : y ∈ Quot.mk Setoid.r l
⊢ 2 ≤ length (Quot.mk Setoid.r l)
case intro.intro.intro.intro
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ length s
induction' s using Quot.inductionOn with l
case intro.intro.intro.intro.h.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hx : x ∈ Quot.mk Setoid.r []
hy : y ∈ Quot.mk Setoid.r []
⊢ 2 ≤ length (Quot.mk Setoid.r [])

case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x ∈ Quot.mk Setoid.r [hd]
hy : y ∈ Quot.mk Setoid.r [hd]
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])

case intro.intro.intro.intro.h.cons.cons
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd hd' : α
tl : List α
hx : x ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
hy : y ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk Setoid.r (hd :: hd' :: tl))
case intro.intro.intro.intro.h
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
hy : y ∈ Quot.mk Setoid.r l
⊢ 2 ≤ length (Quot.mk Setoid.r l)
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
no goals
case intro.intro.intro.intro.h.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hx : x ∈ Quot.mk Setoid.r []
hy : y ∈ Quot.mk Setoid.r []
⊢ 2 ≤ length (Quot.mk Setoid.r [])
simp at hx
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x ∈ Quot.mk Setoid.r [hd]
hy : y ∈ Quot.mk Setoid.r [hd]
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
no goals
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])
simp [hx, hy] at hxy
no goals
case intro.intro.intro.intro.h.cons.cons
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd hd' : α
tl : List α
hx : x ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
hy : y ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk Setoid.r (hd :: hd' :: tl))
simp [Nat.succ_le_succ_iff]