exact Nat.le_antisymm (Nat.le_of_succ_le_succ h) (Nat.ge_of_not_lt h')
α : 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 < Nat.succ n
h' : ¬i < n
⊢ i = n
no goals