n : ℕ
x : Fin (n + 2)
hx' : ↑(finRotate (n + 2)) x ≠ x
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
n : ℕ
⊢ IsCycle (finRotate (n + 2))
refine' ⟨0, by simp, fun x hx' => ⟨x, _⟩⟩
n : ℕ
x : Fin (n + 2)
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
n : ℕ
x : Fin (n + 2)
hx' : ↑(finRotate (n + 2)) x ≠ x
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
clear hx'
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(finRotate (n + 2) ^ ↑↑{ val := x, isLt := hx }) 0 = { val := x, isLt := hx }
n : ℕ
x : Fin (n + 2)
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
cases' x with x hx
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(finRotate (n + 2) ^ ↑↑{ val := x, isLt := hx }) 0 = { val := x, isLt := hx }
rw [zpow_ofNat, Fin.ext_iff, Fin.val_mk]
case mk.zero
n x : ℕ
hx✝ : x < n + 2
hx : Nat.zero < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.zero, isLt := hx }) 0) = ↑{ val := Nat.zero, isLt := hx }

case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.succ x, isLt := hx }) 0) = ↑{ val := Nat.succ x, isLt := hx }
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
induction' x with x ih
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.succ x, isLt := hx }) 0) = ↑{ val := Nat.succ x, isLt := hx }
rw [pow_succ, Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ¬↑{ val := x, isLt := (_ : x < n + 2) } = n + 1
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
rw [Ne.def, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
no goals
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ¬↑{ val := x, isLt := (_ : x < n + 2) } = n + 1
exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)
no goals
n : ℕ
⊢ ↑(finRotate (n + 2)) 0 ≠ 0
simp
no goals
case mk.zero
n x : ℕ
hx✝ : x < n + 2
hx : Nat.zero < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.zero, isLt := hx }) 0) = ↑{ val := Nat.zero, isLt := hx }
rfl