Theorem: quickSortImpl.simp_base (QuickSortInLean/Induction.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ quickSortImpl arr first last = arr
Tactic:
unfold quickSortImpl
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    arr

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    arr
Tactic:
simp [*]
State after:
no goals