case intro
m n : ℕ
i : Fin n
h : ↑Fin.castSucc i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) (↑Fin.castSucc i) = some (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n))
m n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) i = some (Fin.castLT i (_ : ↑i < n))
rcases Fin.exists_castSucc_eq.2 h with ⟨i, rfl⟩
case intro
m n : ℕ
i : Fin n
h : ↑Fin.castSucc i ≠ Fin.last n
⊢ some i = some (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n))
case intro
m n : ℕ
i : Fin n
h : ↑Fin.castSucc i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) (↑Fin.castSucc i) = some (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n))
rw [finSuccEquiv'_last_apply_castSucc]
no goals
case intro
m n : ℕ
i : Fin n
h : ↑Fin.castSucc i ≠ Fin.last n
⊢ some i = some (Fin.castLT (↑Fin.castSucc i) (_ : ↑(↑Fin.castSucc i) < n))
rfl