n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
⊢ False
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑(succAbove p) i ≠ p
intro eq
case pos
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
H : ↑castSucc i < p
⊢ False

case neg
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
H : ¬↑castSucc i < p
⊢ False
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
⊢ False
by_cases H : castSucc i < p
no goals
case pos
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
H : ↑castSucc i < p
⊢ False
simp [lt_irrefl, ← succAbove_below _ _ H, eq] at H
no goals
case neg
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : ↑(succAbove p) i = p
H : ¬↑castSucc i < p
⊢ False
simpa [← succAbove_above _ _ (le_of_not_lt H), eq, H] using castSucc_lt_succ i