case zero
m : ℕ
i : Fin (Nat.zero + 1)
⊢ ↑(finRotate (Nat.zero + 1)) i = i + 1

case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
m n : ℕ
i : Fin (n + 1)
⊢ ↑(finRotate (n + 1)) i = i + 1
cases n
case succ.inl
m n✝ : ℕ
⊢ ↑(finRotate (Nat.succ n✝ + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1

case succ.inr
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
rcases i.le_last.eq_or_lt with (rfl | h)
no goals
case zero
m : ℕ
i : Fin (Nat.zero + 1)
⊢ ↑(finRotate (Nat.zero + 1)) i = i + 1
exact @Subsingleton.elim (Fin 1) _ _ _
no goals
case succ.inl
m n✝ : ℕ
⊢ ↑(finRotate (Nat.succ n✝ + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1
simp [finRotate_last]
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : { val := val✝, isLt := isLt✝ } < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
case succ.inr
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
cases i
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : val✝ < n✝ + 1
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : { val := val✝, isLt := isLt✝ } < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_mk] at h
no goals
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : val✝ < n✝ + 1
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
simp [finRotate_of_lt h, Fin.eq_iff_veq, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]