case intro
m n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : ↑(Fin.succAbove i) j ≠ i
⊢ ↑(finSuccEquiv' i) (↑(Fin.succAbove i) j) = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) (↑(Fin.succAbove i) j))
m n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ ↑(finSuccEquiv' i) j = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) j)
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
case intro.intro
m n : ℕ
j i : Fin n
hi : ↑Fin.castSucc i ≠ Fin.last n
hj : ↑(Fin.succAbove (↑Fin.castSucc i)) j ≠ ↑Fin.castSucc i
⊢ ↑(finSuccEquiv' (↑Fin.castSucc i)) (↑(Fin.succAbove (↑Fin.castSucc i)) j) =
    some
      (Fin.predAbove (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n)) (↑(Fin.succAbove (↑Fin.castSucc i)) j))
case intro
m n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : ↑(Fin.succAbove i) j ≠ i
⊢ ↑(finSuccEquiv' i) (↑(Fin.succAbove i) j) = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) (↑(Fin.succAbove i) j))
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
no goals
case intro.intro
m n : ℕ
j i : Fin n
hi : ↑Fin.castSucc i ≠ Fin.last n
hj : ↑(Fin.succAbove (↑Fin.castSucc i)) j ≠ ↑Fin.castSucc i
⊢ ↑(finSuccEquiv' (↑Fin.castSucc i)) (↑(Fin.succAbove (↑Fin.castSucc i)) j) =
    some
      (Fin.predAbove (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n)) (↑(Fin.succAbove (↑Fin.castSucc i)) j))
simp