exact False.elim <| Nat.le_lt_antisymm this hi
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
hij : i ≥ j
this : len ≤ i
⊢ x[i] = f { val := i, isLt := hi }
no goals