case mk
n m val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑(succ { val := val✝, isLt := isLt✝ }) = ↑{ val := val✝, isLt := isLt✝ } + 1
n m : ℕ
j : Fin n
⊢ ↑(succ j) = ↑j + 1
cases j
no goals
case mk
n m val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑(succ { val := val✝, isLt := isLt✝ }) = ↑{ val := val✝, isLt := isLt✝ } + 1
simp [Fin.succ]