Theorem: partitionImpl.simp_step_ge (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 =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
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)) =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)

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)) =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
Tactic:
simp [*, dbgTraceIfShared]
State after:
no goals