case mk
n m val✝ : ℕ
isLt✝ : val✝ < n + 1
ha : { val := val✝, isLt := isLt✝ } ≠ 0
ha' : optParam (↑castSucc { val := val✝, isLt := isLt✝ } ≠ 0) (_ : ↑castSucc { val := val✝, isLt := isLt✝ } ≠ 0)
⊢ ↑castSucc (pred { val := val✝, isLt := isLt✝ } ha) = pred (↑castSucc { val := val✝, isLt := isLt✝ }) ha'
n m : ℕ
a : Fin (n + 1)
ha : a ≠ 0
ha' : optParam (↑castSucc a ≠ 0) (_ : ↑castSucc a ≠ 0)
⊢ ↑castSucc (pred a ha) = pred (↑castSucc a) ha'
cases a
no goals
case mk
n m val✝ : ℕ
isLt✝ : val✝ < n + 1
ha : { val := val✝, isLt := isLt✝ } ≠ 0
ha' : optParam (↑castSucc { val := val✝, isLt := isLt✝ } ≠ 0) (_ : ↑castSucc { val := val✝, isLt := isLt✝ } ≠ 0)
⊢ ↑castSucc (pred { val := val✝, isLt := isLt✝ } ha) = pred (↑castSucc { val := val✝, isLt := isLt✝ }) ha'
rfl