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}
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ cycleType (cycleRange i) = {↑i + 1}
cases' i with i hi
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}

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}
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}
cases i
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}
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}
rw [cycleRange, cycleType_extendDomain]
no goals
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}
exact cycleType_finRotate
no goals
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}
exact (h0 rfl).elim