case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑(succAbove (pred a ha)) (pred b hb) = pred (↑(succAbove a) b) hk

case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ ↑(succAbove (pred a ha)) (pred b hb) = pred (↑(succAbove a) b) hk
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
⊢ ↑(succAbove (pred a ha)) (pred b hb) = pred (↑(succAbove a) b) hk
obtain hbelow | habove := lt_or_le (castSucc b) a
case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑castSucc (pred b hb) = pred (↑(succAbove a) b) hk

case inl.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑castSucc (pred b hb) < pred a ha
case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑(succAbove (pred a ha)) (pred b hb) = pred (↑(succAbove a) b) hk
rw [Fin.succAbove_below]
no goals
case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑castSucc (pred b hb) = pred (↑(succAbove a) b) hk
rwa [castSucc_pred_eq_pred_castSucc, Fin.pred_inj, Fin.succAbove_below]
no goals
case inl.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
hbelow : ↑castSucc b < a
⊢ ↑castSucc (pred b hb) < pred a ha
rwa [castSucc_pred_eq_pred_castSucc, pred_lt_pred_iff]
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ succ (pred b hb) = pred (↑(succAbove a) b) hk

case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ pred a ha ≤ ↑castSucc (pred b hb)
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ ↑(succAbove (pred a ha)) (pred b hb) = pred (↑(succAbove a) b) hk
rw [Fin.succAbove_above]
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
this : succ (pred b hb) = pred (succ b) (_ : succ b ≠ 0)
⊢ succ (pred b hb) = pred (↑(succAbove a) b) hk

case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ pred a ha ≤ ↑castSucc (pred b hb)
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ succ (pred b hb) = pred (↑(succAbove a) b) hk

case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ pred a ha ≤ ↑castSucc (pred b hb)
have : (b.pred hb).succ = b.succ.pred (Fin.succ_ne_zero _) := by rw [succ_pred, pred_succ]
no goals
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ succ (pred b hb) = pred (succ b) (_ : succ b ≠ 0)
rw [succ_pred, pred_succ]
no goals
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
this : succ (pred b hb) = pred (succ b) (_ : succ b ≠ 0)
⊢ succ (pred b hb) = pred (↑(succAbove a) b) hk
rwa [this, Fin.pred_inj, Fin.succAbove_above]
no goals
case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (↑(succAbove a) b ≠ 0) (_ : ↑(succAbove a) b ≠ 0)
habove : a ≤ ↑castSucc b
⊢ pred a ha ≤ ↑castSucc (pred b hb)
rwa [castSucc_pred_eq_pred_castSucc, Fin.pred_le_pred_iff]