m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(↑(finRotate (n + 1)) i) = ↑i + 1
rw [finRotate_succ_apply]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
have : (i : ℕ) < n := Fin.val_lt_last h
no goals
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
exact Fin.val_add_one_of_lt this