Theorem: partitionImpl.simp_base (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
⊢ ↑first ≤ ↑i
Tactic:
assumption
State after:
no goals

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