n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : ↑castSucc a < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) ≤
    if h : ↑castSucc b < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p => predAbove p i) a ≤ (fun p => predAbove p i) b
dsimp [predAbove]
case inl.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ↑castSucc a < i
hb : ↑castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ pred i (_ : i ≠ 0)

case inl.inr
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ↑castSucc a < i
hb : ¬↑castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ castLT i (_ : ↑i < n)

case inr.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ↑castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)

case inr.inr
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ¬↑castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ castLT i (_ : ↑i < n)
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : ↑castSucc a < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) ≤
    if h : ↑castSucc b < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)
split_ifs with ha hb hb
no goals
case inl.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ↑castSucc a < i
hb : ↑castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ pred i (_ : i ≠ 0)
rfl
no goals
case inl.inr
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ↑castSucc a < i
hb : ¬↑castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ castLT i (_ : ↑i < n)
exact pred_le _
case inr.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ↑castSucc b < i
this : b < a
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)
case inr.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ↑castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)
have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
no goals
case inr.inl
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ↑castSucc b < i
this : b < a
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)
exact absurd H this.not_le
no goals
case inr.inr
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬↑castSucc a < i
hb : ¬↑castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ castLT i (_ : ↑i < n)
rfl