rw [if_neg hi']
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else as[i]) = if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size