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

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

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

case inr.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ castLT b (_ : ↑b < n)
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : ↑castSucc p < a then pred a (_ : a ≠ 0) else castLT a (_ : ↑a < n)) ≤
    if h : ↑castSucc p < b then pred b (_ : b ≠ 0) else castLT b (_ : ↑b < n)
split_ifs with ha hb hb
case inl.inl
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ↑castSucc p < a
hb : ↑castSucc p < b
⊢ ↑a - 1 ≤ ↑b - 1

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

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

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

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

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

case inr.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ castLT b (_ : ↑b < n)
all_goals simp only [le_iff_val_le_val, coe_pred]
case inr.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑(castLT b (_ : ↑b < n))
case inr.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ castLT b (_ : ↑b < n)
simp only [le_iff_val_le_val, coe_pred]
no goals
case inl.inl
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ↑castSucc p < a
hb : ↑castSucc p < b
⊢ ↑a - 1 ≤ ↑b - 1
exact pred_le_pred H
no goals
case inl.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ ↑a - 1 ≤ ↑(castLT b (_ : ↑b < n))
calc
  _ ≤ _ := Nat.pred_le _
  _ ≤ _ := H
case inr.inl
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha✝ : ¬↑castSucc p < a
hb : ↑castSucc p < b
ha : a ≤ ↑castSucc p
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑b - 1
case inr.inl
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ↑castSucc p < b
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑b - 1
simp at ha
no goals
case inr.inl
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha✝ : ¬↑castSucc p < a
hb : ↑castSucc p < b
ha : a ≤ ↑castSucc p
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑b - 1
exact le_pred_of_lt (lt_of_le_of_lt ha hb)
no goals
case inr.inr
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬↑castSucc p < a
hb : ¬↑castSucc p < b
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑(castLT b (_ : ↑b < n))
exact H