next hne =>
  have hi : i < n := Nat.lt_of_le_of_ne hi hne
  simp only at h
  split at h
  next hp =>
    contradiction
  next hp =>
    by_cases i = k.val with
    | isTrue heq =>
      rw [Bool.eq_false_iff]
      intro hk
      apply hp
      rw [←hk]
      congr
    | isFalse hik' =>
      have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
      exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
no goals