case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ↑p x = x
⊢ Nodup (toList p x)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
⊢ Nodup (toList p x)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
⊢ Nodup (toList p x)
by_cases hx : p x = x
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ Nodup (toList p x)
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
⊢ Nodup (toList p x)
have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ ∀ (i j : ℕ) (h₁ : i < length (toList p x)) (h₂ : j < length (toList p x)),
    nthLe (toList p x) i h₁ = nthLe (toList p x) j h₂ → i = j
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ Nodup (toList p x)
rw [nodup_iff_nthLe_inj]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn : n < length (toList p x)
hm : m < length (toList p x)
⊢ nthLe (toList p x) n hn = nthLe (toList p x) m hm → n = m
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ ∀ (i j : ℕ) (h₁ : i < length (toList p x)) (h₂ : j < length (toList p x)),
    nthLe (toList p x) i h₁ = nthLe (toList p x) j h₂ → i = j
rintro n m hn hm
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn : n < length (toList p x)
hm : m < length (toList p x)
⊢ nthLe (toList p x) n hn = nthLe (toList p x) m hm → n = m
rw [length_toList, ← hc.orderOf] at hm hn
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
rw [← cycleOf_apply_self, ← Ne.def, ← mem_support] at hx
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ n) x = ↑(cycleOf p x ^ m) x → n = m
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
rw [nthLe_toList, nthLe_toList, ← cycleOf_pow_apply_self p x n, ←
  cycleOf_pow_apply_self p x m]
case neg.zero.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.zero = Nat.zero

case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m

case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero

case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.succ n = Nat.succ m
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ n) x = ↑(cycleOf p x ^ m) x → n = m
cases' n with n <;> cases' m with m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
⊢ Nat.succ n = Nat.succ m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.succ n = Nat.succ m
intro h
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
⊢ Nat.succ n = Nat.succ m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
⊢ Nat.succ n = Nat.succ m
have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
hm' : ¬orderOf (cycleOf p x) ∣ Nat.succ m
⊢ Nat.succ n = Nat.succ m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
⊢ Nat.succ n = Nat.succ m
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ Nat.succ n = Nat.succ m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
hm' : ¬orderOf (cycleOf p x) ∣ Nat.succ m
⊢ Nat.succ n = Nat.succ m
rw [← hc.support_pow_eq_iff] at hn' hm'
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ cycleOf p x ^ Nat.succ n = cycleOf p x ^ Nat.succ m
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ Nat.succ n = Nat.succ m
rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]
case neg.succ.succ.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ support (cycleOf p x ^ Nat.succ n) ⊆ support (cycleOf p x ^ Nat.succ m)

case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α),
    x_1 ∈ support (cycleOf p x ^ Nat.succ m) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ cycleOf p x ^ Nat.succ n = cycleOf p x ^ Nat.succ m
refine' support_congr _ _
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝ : ↑p x = x
hx : toList p x = []
⊢ Nodup (toList p x)
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ↑p x = x
⊢ Nodup (toList p x)
rw [← not_mem_support, ← toList_eq_nil_iff] at hx
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝ : ↑p x = x
hx : toList p x = []
⊢ Nodup (toList p x)
simp [hx]
no goals
case neg.zero.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.zero = Nat.zero
simp
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hx : ↑(p ^ Nat.succ m) x ≠ x
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m
rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support,
  cycleOf_pow_apply_self] at hx
no goals
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hx : ↑(p ^ Nat.succ m) x ≠ x
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m
simp [hx.symm]
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
n : ℕ
hx : ↑(p ^ Nat.succ n) x ≠ x
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
  cycleOf_pow_apply_self] at hx
no goals
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
n : ℕ
hx : ↑(p ^ Nat.succ n) x ≠ x
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero
simp [hx]
no goals
case neg.succ.succ.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ support (cycleOf p x ^ Nat.succ n) ⊆ support (cycleOf p x ^ Nat.succ m)
rw [hm', hn']
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α), x_1 ∈ support (cycleOf p x) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α),
    x_1 ∈ support (cycleOf p x ^ Nat.succ m) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
rw [hm']
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
y : α
hy : y ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) y = ↑(cycleOf p x ^ Nat.succ m) y
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α), x_1 ∈ support (cycleOf p x) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
intro y hy
case neg.succ.succ.refine'_2.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
k : ℕ
hy : ↑(cycleOf p x ^ k) x ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) (↑(cycleOf p x ^ k) x) = ↑(cycleOf p x ^ Nat.succ m) (↑(cycleOf p x ^ k) x)
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
y : α
hy : y ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) y = ↑(cycleOf p x ^ Nat.succ m) y
obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
no goals
case neg.succ.succ.refine'_2.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
k : ℕ
hy : ↑(cycleOf p x ^ k) x ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) (↑(cycleOf p x ^ k) x) = ↑(cycleOf p x ^ Nat.succ m) (↑(cycleOf p x ^ k) x)
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
  (Commute.pow_pow_self _ _ _).eq]