simp [*] at *
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j.prev) swapped (partitionImpl swapped first i.prev j.prev jl ⋯).snd)
⊢ Nonempty
    (permuted n (↑first) (↑j) arr
      (if h : first < i then
          let_fun this := ⋯;
          if arr[i] < arr[first] then
            let_fun this_1 := ⋯;
            partitionImpl arr first i.prev j this this_1
          else
            let arr := (dbgTraceIfShared "swap1" arr).swap i j;
            match partitionImpl arr first i.prev j.prev this ⋯ with
            | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
        else (⟨j, ⋯⟩, arr)).snd)
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')