suffices i = n by cases this; rfl
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ i = n