case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := i, isLt := hi })
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ IsCycle (cycleRange i)
cases' i with i hi
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.zero, isLt := hi })

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 })
case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := i, isLt := hi })
cases i
no goals
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 })
exact isCycle_finRotate.extendDomain _
no goals
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.zero, isLt := hi })
exact (h0 rfl).elim