case inl
n : ℕ
i j : Fin (Nat.succ n)
h₁ : j < i
⊢ ↑(cycleRange i) j = j + 1

case inr.inl
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : j = i
⊢ ↑(cycleRange i) j = 0

case inr.inr
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : ¬j = i
⊢ ↑(cycleRange i) j = j
n : ℕ
i j : Fin (Nat.succ n)
⊢ ↑(cycleRange i) j = if j < i then j + 1 else if j = i then 0 else j
split_ifs with h₁ h₂
no goals
case inl
n : ℕ
i j : Fin (Nat.succ n)
h₁ : j < i
⊢ ↑(cycleRange i) j = j + 1
exact cycleRange_of_lt h₁
no goals
case inr.inl
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : j = i
⊢ ↑(cycleRange i) j = 0
exact cycleRange_of_eq h₂
no goals
case inr.inr
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : ¬j = i
⊢ ↑(cycleRange i) j = j
exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))