n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (if h : ↑castSucc 0 < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n + 1)) = pred i hi
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ predAbove 0 i = pred i hi
dsimp [predAbove]
case hc
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ↑castSucc 0 < i
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (if h : ↑castSucc 0 < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n + 1)) = pred i hi
rw [dif_pos]
case hc
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ 0 < i
case hc
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ↑castSucc 0 < i
simp only [castSucc_zero]
no goals
case hc
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ 0 < i
exact (pos_iff_ne_zero _).mpr hi