case mk
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ ↑(castPred { val := a, isLt := ha }) = ↑{ val := a, isLt := ha }
n✝ m n : ℕ
a : Fin (n + 2)
hx : a < last (n + 1)
⊢ ↑(castPred a) = ↑a
rcases a with ⟨a, ha⟩
case mk.h
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ a < n + 1
case mk
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ ↑(castPred { val := a, isLt := ha }) = ↑{ val := a, isLt := ha }
rw [castPred_mk]
no goals
case mk.h
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ a < n + 1
exact hx