m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x) = some (Fin.castLT ↑x (_ : ↑↑x < n))
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ ↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x = Fin.castLT ↑x (_ : ↑↑x < n)
rw [← Option.some_inj]
no goals
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x) = some (Fin.castLT ↑x (_ : ↑↑x < n))
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_last_apply x.property