-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem isCycle_formPerm (hl : Nodup l) (hn : 2 ≤ l.length) : IsCycle (formPerm l)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
⊢ (x :: l).formPerm.IsCycle

Tactic:
induction' l with y l generalizing x

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
hl : [x].Nodup
hn : 2 ≤ [x].length
⊢ [x].formPerm.IsCycle

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm.IsCycle

Proof state:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
⊢ (x :: y :: l).formPerm.SameCycle x w

Tactic:
have : w ∈ x::y::l := mem_of_formPerm_ne_self _ _ hw

Result:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
this : w ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x w

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
hn : 2 ≤ [].length
⊢ [].formPerm.IsCycle

Tactic:
norm_num at hn

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm.IsCycle

Tactic:
use x

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x ∧ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ l.formPerm.IsCycle

Tactic:
rcases l with - | ⟨x, l⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
hn : 2 ≤ [].length
⊢ [].formPerm.IsCycle

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

Proof state:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
this : w ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x w

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem this

Result:
case h.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x (x :: y :: l)[k]

Proof state:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Tactic:
intro w hw

Result:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
⊢ (x :: y :: l).formPerm.SameCycle x w

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
hl : [x].Nodup
hn : 2 ≤ [x].length
⊢ [x].formPerm.IsCycle

Tactic:
norm_num at hn

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x ∧ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Tactic:
constructor

Result:
case h.left
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x

case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Proof state:
case h.left
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x

Tactic:
rwa [formPerm_apply_mem_ne_self_iff _ hl _ (mem_cons_self _ _)]

Result:
no goals

Proof state:
case h.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x (x :: y :: l)[k]

Tactic:
use k

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ ((x :: y :: l).formPerm ^ ↑k) x = (x :: y :: l)[k]

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ ((x :: y :: l).formPerm ^ ↑k) x = (x :: y :: l)[k]

Tactic:
simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]

Result:
no goals