case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl : Nodup []
hn : 2 ≤ length []
⊢ IsCycle (formPerm [])

case cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x : α
l : List α
hl : Nodup (x :: l)
hn : 2 ≤ length (x :: l)
⊢ IsCycle (formPerm (x :: l))
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length l
⊢ IsCycle (formPerm l)
cases' l with x l
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l : List α
hl✝ : Nodup (x✝ :: l)
hn✝ : 2 ≤ length (x✝ :: l)
x : α
hl : Nodup [x]
hn : 2 ≤ length [x]
⊢ IsCycle (formPerm [x])

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ IsCycle (formPerm (x :: y :: l))
case cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x : α
l : List α
hl : Nodup (x :: l)
hn : 2 ≤ length (x :: l)
⊢ IsCycle (formPerm (x :: l))
induction' l with y l generalizing x
no goals
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl : Nodup []
hn : 2 ≤ length []
⊢ IsCycle (formPerm [])
norm_num at hn
no goals
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l : List α
hl✝ : Nodup (x✝ :: l)
hn✝ : 2 ≤ length (x✝ :: l)
x : α
hl : Nodup [x]
hn : 2 ≤ length [x]
⊢ IsCycle (formPerm [x])
norm_num at hn
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ IsCycle (formPerm (x :: y :: l))
use x
case cons.cons.left
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x

case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
constructor
no goals
case cons.cons.left
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x
rwa [formPerm_apply_mem_ne_self_iff _ hl _ (mem_cons_self _ _)]
case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
⊢ SameCycle (formPerm (x :: y :: l)) x w
case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
intro w hw
case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
this : w ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x w
case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
⊢ SameCycle (formPerm (x :: y :: l)) x w
have : w ∈ x::y::l := mem_of_formPerm_ne_self _ _ hw
case cons.cons.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x (nthLe (x :: y :: l) k hk)
case cons.cons.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
this : w ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x w
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem this
case cons.cons.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ ↑(formPerm (x :: y :: l) ^ ↑k) x = nthLe (x :: y :: l) k hk
case cons.cons.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x (nthLe (x :: y :: l) k hk)
use k
no goals
case cons.cons.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ ↑(formPerm (x :: y :: l) ^ ↑k) x = nthLe (x :: y :: l) k hk
simp only [zpow_ofNat, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]