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

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  quickSortImpl arr first last = quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last
Tactic:
rw [quickSortImpl]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  (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) =
    quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  (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) =
    quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last
Tactic:
simp [*]
State after:
no goals