Theorem: Fin.castSucc_le_succAbove (Controlbits/Fin.lean)

State before:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc ≤ p.succAbove i
Tactic:
obtain h | h := succAbove_eq_castSucc_or_succ p i <;> rw [h]
State after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.succ
⊢ i.castSucc ≤ i.succ

State before:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.succ
⊢ i.castSucc ≤ i.succ
Tactic:
exact (castSucc_lt_succ _).le
State after:
no goals