have hsucc : ⟨i+1, hi⟩ = Fin.succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ := rfl
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩