case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
⊢ ↑(cycleRange i) (↑(succAbove i) j) = succ j

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
⊢ ↑(cycleRange i) (↑(succAbove i) j) = succ j
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ↑(cycleRange i) (↑(succAbove i) j) = succ j
cases' lt_or_ge (castSucc j) i with h h
no goals
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
⊢ ↑(cycleRange i) (↑(succAbove i) j) = succ j
rw [Fin.succAbove_below _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
no goals
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
⊢ ↑(cycleRange i) (↑(succAbove i) j) = succ j
rw [Fin.succAbove_above _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]