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