case zero
i j : Fin (Nat.succ Nat.zero)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1

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
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
cases n
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
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
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
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)
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
ext
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)
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)
erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
  Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
  viaFintypeEmbedding_apply_image, coe_castLE, coe_finRotate]
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)
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)
simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
case succ.h.inl
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

case succ.h.inr
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)
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)
split_ifs with heq
no goals
case zero
i j : Fin (Nat.succ Nat.zero)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
exact Subsingleton.elim (α := Fin 1) _ _
no goals
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) }
simp
no goals
case succ.h.inl
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
rfl
case succ.h.inr
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)
case succ.h.inr
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)
rw [Fin.val_add_one_of_lt]
no goals
case succ.h.inr
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)
exact lt_of_lt_of_le (lt_of_le_of_ne h (mt (congr_arg _) heq)) (le_last i)