[GOAL]
n : ℕ
p : Fin (n + 1)
⊢ ↑decomposeFin.symm (p, Equiv.refl (Fin n)) = swap 0 p
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]
[GOAL]
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑(↑decomposeFin.symm (p, e)) 0 = p
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin]
[GOAL]
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (p, e)) (Fin.succ x) = ↑(swap 0 p) (Fin.succ (↑e x))
[PROOFSTEP]
refine' Fin.cases _ _ p
[GOAL]
case refine'_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (0, e)) (Fin.succ x) = ↑(swap 0 0) (Fin.succ (↑e x))
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, EquivFunctor.map]
[GOAL]
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
by_cases h : i = e x
[GOAL]
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map]
[GOAL]
case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
simp [h, Fin.succ_ne_zero, Equiv.Perm.decomposeFin, EquivFunctor.map, swap_apply_def, Ne.symm h]
[GOAL]
n : ℕ
e : Perm (Fin (n + 1))
p : Fin (n + 2)
⊢ ↑(↑decomposeFin.symm (p, e)) 1 = ↑(swap 0 p) (Fin.succ (↑e 0))
[PROOFSTEP]
rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]
[GOAL]
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑sign (↑decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
refine' Fin.cases _ _ p
[GOAL]
case refine'_1
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑sign (↑decomposeFin.symm (0, e)) = (if 0 = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Fin.succ_ne_zero]
[GOAL]
case refine'_2
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ∀ (i : Fin n), ↑sign (↑decomposeFin.symm (Fin.succ i, e)) = (if Fin.succ i = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Fin.succ_ne_zero]
[GOAL]
n : ℕ
⊢ finRotate (Nat.succ n) = ↑decomposeFin.symm (1, finRotate n)
[PROOFSTEP]
ext i
[GOAL]
case H.h
n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate n)) i)
[PROOFSTEP]
cases n
[GOAL]
case H.h.zero
i : Fin (Nat.succ Nat.zero)
⊢ ↑(↑(finRotate (Nat.succ Nat.zero)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate Nat.zero)) i)
[PROOFSTEP]
simp
[GOAL]
case H.h.succ
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) i) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) i)
[PROOFSTEP]
refine' Fin.cases _ (fun i => _) i
[GOAL]
case H.h.succ.refine'_1
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) 0) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) 0)
[PROOFSTEP]
simp
[GOAL]
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) (Fin.succ i)) =
    ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) (Fin.succ i))
[PROOFSTEP]
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
[GOAL]
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑(Fin.succ i) + 1) = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑(Fin.succ i) + 1 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate, if_neg h, Fin.val_zero,
  Fin.val_one, swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
[GOAL]
n : ℕ
⊢ ↑sign (finRotate (n + 1)) = (-1) ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ ↑sign (finRotate (Nat.zero + 1)) = (-1) ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (finRotate (Nat.succ n + 1)) = (-1) ^ Nat.succ n
[PROOFSTEP]
rw [finRotate_succ_eq_decomposeFin]
[GOAL]
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (↑decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ Nat.succ n
[PROOFSTEP]
simp [ih, pow_succ]
[GOAL]
n : ℕ
⊢ support (finRotate (n + 2)) = Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ support (finRotate (n + 2)) ↔ a✝ ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ support (finRotate n) = Finset.univ
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ support (finRotate (2 + m)) = Finset.univ
[PROOFSTEP]
rw [add_comm, support_finRotate]
[GOAL]
n : ℕ
⊢ IsCycle (finRotate (n + 2))
[PROOFSTEP]
refine' ⟨0, by simp, fun x hx' => ⟨x, _⟩⟩
[GOAL]
n : ℕ
⊢ ↑(finRotate (n + 2)) 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
x : Fin (n + 2)
hx' : ↑(finRotate (n + 2)) x ≠ x
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
[PROOFSTEP]
clear hx'
[GOAL]
n : ℕ
x : Fin (n + 2)
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(finRotate (n + 2) ^ ↑↑{ val := x, isLt := hx }) 0 = { val := x, isLt := hx }
[PROOFSTEP]
rw [zpow_ofNat, Fin.ext_iff, Fin.val_mk]
[GOAL]
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
[PROOFSTEP]
induction' x with x ih
[GOAL]
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 }
[PROOFSTEP]
rfl
[GOAL]
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 }
[PROOFSTEP]
rw [pow_succ, Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
[GOAL]
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)
[PROOFSTEP]
rw [Ne.def, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
[GOAL]
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
[PROOFSTEP]
exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ IsCycle (finRotate n)
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (2 + m))
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (m + 2))
[PROOFSTEP]
exact isCycle_finRotate
[GOAL]
n : ℕ
⊢ cycleType (finRotate (n + 2)) = {n + 2}
[PROOFSTEP]
rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
[GOAL]
n : ℕ
⊢ ↑[n + 2] = {n + 2}
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ cycleType (finRotate n) = {n}
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ cycleType (finRotate (2 + m)) = {2 + m}
[PROOFSTEP]
rw [add_comm, cycleType_finRotate]
[GOAL]
n : ℕ
i : Fin n
⊢ Function.LeftInverse (fun x => ↑↑x) ↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
i : Fin n
x : Fin (Nat.succ ↑i)
⊢ (fun x => ↑↑x) (↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding x) = x
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
i : Fin n
x : Fin (Nat.succ ↑i)
⊢ ↑((fun x => ↑↑x) (↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding x)) = ↑x
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : i < j
⊢ ↑(cycleRange i) j = j
[PROOFSTEP]
rw [cycleRange, ofLeftInverse'_eq_ofInjective, ← Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
  viaFintypeEmbedding_apply_not_mem_range]
[GOAL]
case h
n : ℕ
i j : Fin (Nat.succ n)
h : i < j
⊢ ¬j ∈ Set.range ↑(castLEEmb (_ : Nat.succ ↑i ≤ Nat.succ n)).toEmbedding
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
i j : Fin (Nat.succ Nat.zero)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
exact
  Subsingleton.elim (α := Fin 1) _
    _
      --Porting note; was `simp`
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt)) ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ := by simp
[GOAL]
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
⊢ j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
ext
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ ↑(↑(cycleRange i) j) = ↑(if j = i then 0 else j + 1)
[PROOFSTEP]
erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ← Function.Embedding.toEquivRange_eq_ofInjective, ←
  viaFintypeEmbedding, viaFintypeEmbedding_apply_image, castLEEmb_toEmbedding, Function.Embedding.coeFn_mk, coe_castLE,
  coe_finRotate]
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ (if { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } = last ↑i then 0
    else ↑{ val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } + 1) =
    ↑(if castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } = i then 0
      else castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } + 1)
[PROOFSTEP]
simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ (if ↑j = ↑i then 0 else ↑j + 1) = ↑(if ↑j = ↑i then 0 else j + 1)
[PROOFSTEP]
split_ifs with heq
[GOAL]
case pos
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ↑j = ↑i
⊢ 0 = ↑0
[PROOFSTEP]
rfl
[GOAL]
case neg
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ¬↑j = ↑i
⊢ ↑j + 1 = ↑(j + 1)
[PROOFSTEP]
rw [Fin.val_add_one_of_lt]
[GOAL]
case neg
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ¬↑j = ↑i
⊢ j < last (n✝ + 1)
[PROOFSTEP]
exact lt_of_lt_of_le (lt_of_le_of_ne h (mt (congr_arg _) heq)) (le_last i)
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(↑(cycleRange i) j) = if j = i then 0 else ↑j + 1
[PROOFSTEP]
rw [cycleRange_of_le h]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1
[PROOFSTEP]
exact
  val_add_one_of_lt
    (calc
      (j : ℕ) < i := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
      _ ≤ n := Nat.lt_succ_iff.mp i.2)
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j < i
⊢ ↑(cycleRange i) j = j + 1
[PROOFSTEP]
rw [cycleRange_of_le h.le, if_neg h.ne]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j < i
⊢ ↑(↑(cycleRange i) j) = ↑j + 1
[PROOFSTEP]
rw [coe_cycleRange_of_le h.le, if_neg h.ne]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j = i
⊢ ↑(cycleRange i) j = 0
[PROOFSTEP]
rw [cycleRange_of_le h.le, if_pos h]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
⊢ ↑(cycleRange i) j = if j < i then j + 1 else if j = i then 0 else j
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h₁ : j < i
⊢ ↑(cycleRange i) j = j + 1
[PROOFSTEP]
exact cycleRange_of_lt h₁
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : j = i
⊢ ↑(cycleRange i) j = 0
[PROOFSTEP]
exact cycleRange_of_eq h₂
[GOAL]
case neg
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : ¬j = i
⊢ ↑(cycleRange i) j = j
[PROOFSTEP]
exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))
[GOAL]
n : ℕ
⊢ cycleRange 0 = 1
[PROOFSTEP]
ext j
[GOAL]
case H.h
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) j) = ↑(↑1 j)
[PROOFSTEP]
refine' Fin.cases _ (fun j => _) j
[GOAL]
case H.h.refine'_1
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) 0) = ↑(↑1 0)
[PROOFSTEP]
simp
[GOAL]
case H.h.refine'_2
n : ℕ
j✝ : Fin (Nat.succ n)
j : Fin n
⊢ ↑(↑(cycleRange 0) (succ j)) = ↑(↑1 (succ j))
[PROOFSTEP]
rw [cycleRange_of_gt (Fin.succ_pos j), one_apply]
[GOAL]
n : ℕ
⊢ cycleRange (last n) = finRotate (n + 1)
[PROOFSTEP]
ext i
[GOAL]
case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑(↑(cycleRange (last n)) i) = ↑(↑(finRotate (n + 1)) i)
[PROOFSTEP]
rw [coe_cycleRange_of_le (le_last _), coe_finRotate]
[GOAL]
n : ℕ
h : 0 < n
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
h : 0 < Nat.zero
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
cases h
[GOAL]
case succ
n : ℕ
h : 0 < Nat.succ n
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
exact cycleRange_zero n
[GOAL]
n : ℕ
i : Fin n
⊢ ↑sign (cycleRange i) = (-1) ^ ↑i
[PROOFSTEP]
simp [cycleRange]
[GOAL]
n : ℕ
i j : Fin n
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
cases n
[GOAL]
case zero
i j : Fin Nat.zero
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rcases j with ⟨_, ⟨⟩⟩
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ n✝)
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rcases lt_trichotomy j i with (hlt | heq | hgt)
[GOAL]
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
have : castSucc (j + 1) = j.succ := by
  ext
  rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
[GOAL]
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ castSucc (j + 1) = succ j
[PROOFSTEP]
ext
[GOAL]
case h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(castSucc (j + 1)) = ↑(succ j)
[PROOFSTEP]
rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
[GOAL]
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_below, this, swap_apply_of_ne_of_ne]
[GOAL]
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succ j ≠ 0
[PROOFSTEP]
apply Fin.succ_ne_zero
[GOAL]
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succ j ≠ succ i
[PROOFSTEP]
exact (Fin.succ_injective _).ne hlt.ne
[GOAL]
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ castSucc (j + 1) < succ i
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val]
[GOAL]
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ ↑(castSucc (j + 1)) < ↑(succ i)
[PROOFSTEP]
simpa [this] using hlt
[GOAL]
case succ.inr.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [heq, Fin.cycleRange_self, Fin.succAbove_below, swap_apply_right, Fin.castSucc_zero]
[GOAL]
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ castSucc 0 < succ i
[PROOFSTEP]
rw [Fin.castSucc_zero]
[GOAL]
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ 0 < succ i
[PROOFSTEP]
apply Fin.succ_pos
[GOAL]
case succ.inr.inr
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_above, swap_apply_of_ne_of_ne]
[GOAL]
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ 0
[PROOFSTEP]
apply Fin.succ_ne_zero
[GOAL]
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ succ i
[PROOFSTEP]
apply (Fin.succ_injective _).ne hgt.ne.symm
[GOAL]
case succ.inr.inr.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ i ≤ castSucc j
[PROOFSTEP]
simpa [Fin.le_iff_val_le_val] using hgt
[GOAL]
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
cases' lt_or_ge (castSucc j) i with h h
[GOAL]
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
rw [Fin.succAbove_below _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
[GOAL]
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
rw [Fin.succAbove_above _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ ↑(cycleRange i) (↑(cycleRange i).symm 0) = ↑(cycleRange i) i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ↑(cycleRange i) (↑(cycleRange i).symm (succ j)) = ↑(cycleRange i) (succAbove i j)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ IsCycle (cycleRange i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := i, isLt := hi })
[PROOFSTEP]
cases i
[GOAL]
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.zero, isLt := hi })
[PROOFSTEP]
exact (h0 rfl).elim
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.succ n✝, isLt := hi })
[PROOFSTEP]
exact isCycle_finRotate.extendDomain _
[GOAL]
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ cycleType (cycleRange i) = {↑i + 1}
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := i, isLt := hi }) = {↑{ val := i, isLt := hi } + 1}
[PROOFSTEP]
cases i
[GOAL]
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := Nat.zero, isLt := hi }) = {↑{ val := Nat.zero, isLt := hi } + 1}
[PROOFSTEP]
exact (h0 rfl).elim
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := Nat.succ n✝, isLt := hi }) = {↑{ val := Nat.succ n✝, isLt := hi } + 1}
[PROOFSTEP]
rw [cycleRange, cycleType_extendDomain]
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ cycleType (finRotate (↑{ val := Nat.succ n✝, isLt := hi } + 1)) = {↑{ val := Nat.succ n✝, isLt := hi } + 1}
[PROOFSTEP]
exact cycleType_finRotate
[GOAL]
n : ℕ
⊢ IsThreeCycle (cycleRange 2)
[PROOFSTEP]
rw [IsThreeCycle, cycleType_cycleRange]
[GOAL]
n : ℕ
⊢ {↑2 + 1} = {3}
[PROOFSTEP]
simp [Fin.eq_iff_veq]
[GOAL]
n : ℕ
⊢ 2 ≠ 0
[PROOFSTEP]
simp [Fin.eq_iff_veq]
