Theorem: partitionImpl.simp_step_lt (QuickSortInLean/Induction.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ partitionImpl arr first i j fi ij = partitionImpl arr first i.prev j ⋯ ⋯
Tactic:
rw [partitionImpl]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ (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)) =
    partitionImpl arr first i.prev j ⋯ ⋯

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ (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)) =
    partitionImpl arr first i.prev j ⋯ ⋯
Tactic:
simp [*]
State after:
no goals