Theorem: partition.partition (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let afterLoop := partitionImpl arr first last last fl (Nat.le_refl _)
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let mid := afterLoop.1
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let arr' := afterLoop.2
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have : mid < n := Nat.lt_of_le_of_lt mid.property.2 last.isLt
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let swapped := arr'.swap first ⟨mid, by assumption⟩
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have : result.1 = mid := by
  rw [←eq]
  unfold partition
  simp [afterLoop]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have : result.2 = swapped := by
  rw [←eq]
  unfold partition
  simp [afterLoop, dbgTraceIfShared]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have first_eq : arr'[first] = arr[first] := by
  apply partitionImpl.first_eq
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let inv₀ : partitionImpl.LoopInvariant arr first last last last := by
  apply partitionImpl.LoopInvariant.intro
  . intro k lk kl
    exact (Nat.lt_irrefl k (Nat.lt_trans kl lk)).elim
  . intro k lk kl
    exact (Nat.lt_irrefl k (Nat.lt_of_le_of_lt kl lk)).elim
  . intro ll
    exact (Nat.lt_irrefl last ll).elim
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
let inv := partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl _) inv₀ afterLoop (by rfl)
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have p₁ (k : Fin n) (fk : first ≤ k) (km : k.val < mid) : swapped[k] <o arr[first] := by
  cases Nat.eq_or_lt_of_le fk with
  | inl fk =>
    have : swapped[k] = swapped[first] := by
      simp [Fin.eq_of_val_eq fk]
    rw [this]
    have : swapped[first] = arr'[mid.val] := by
      apply Vec.get_swap_left
    rw [this, ←first_eq]
    exact inv.3 (Fin.eq_of_val_eq fk ▸ km)
  | inr fk =>
    have : swapped[k] = arr'[k] := by
      apply Vec.get_swap_neq
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_gt fk
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_lt km
    rw [this, ←first_eq]
    exact inv.1 k fk km
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have p₂ : swapped[mid.val] = arr[first] := by
  have : swapped[mid.val] = arr'[first] := by
    apply Vec.get_swap_right
  rw [this]
  assumption
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
have p₃ (k : Fin n) (mk : mid < k.val) (kl : k ≤ last) : ¬swapped[k] <o arr[first] := by
  have : swapped[k] = arr'[k] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt (Nat.lt_of_le_of_lt mid.property.1 mk)
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt mk
  rw [this, ←first_eq]
  exact inv.2 k mk kl
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
apply And.intro
State after:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first] ∧ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first] ∧ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
. simp [*]
  apply p₁
State after:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first] ∧ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first] ∧ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
. apply And.intro
  . simp [*]
  . simp [*]
    apply p₃
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
⊢ ↑mid.val < n
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ result.fst = mid
Tactic:
rw [←eq]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (_root_.partition arr first last fl).fst = mid

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (_root_.partition arr first last fl).fst = mid
Tactic:
unfold partition
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (let result := partitionImpl arr first last last fl ⋯;
      let mid := result.fst;
      let arr_1 := result.snd;
      (mid, (dbgTraceIfShared "swap2" arr_1).swap first ⟨↑mid.val, ⋯⟩)).fst =
    mid

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this⟩
⊢ (let result := partitionImpl arr first last last fl ⋯;
      let mid := result.fst;
      let arr_1 := result.snd;
      (mid, (dbgTraceIfShared "swap2" arr_1).swap first ⟨↑mid.val, ⋯⟩)).fst =
    mid
Tactic:
simp [afterLoop]
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ result.snd = swapped
Tactic:
rw [←eq]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (_root_.partition arr first last fl).snd = swapped

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (_root_.partition arr first last fl).snd = swapped
Tactic:
unfold partition
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (let result := partitionImpl arr first last last fl ⋯;
      let mid := result.fst;
      let arr_1 := result.snd;
      (mid, (dbgTraceIfShared "swap2" arr_1).swap first ⟨↑mid.val, ⋯⟩)).snd =
    swapped

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (let result := partitionImpl arr first last last fl ⋯;
      let mid := result.fst;
      let arr_1 := result.snd;
      (mid, (dbgTraceIfShared "swap2" arr_1).swap first ⟨↑mid.val, ⋯⟩)).snd =
    swapped
Tactic:
simp [afterLoop, dbgTraceIfShared]
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
⊢ arr'[first] = arr[first]
Tactic:
apply partitionImpl.first_eq
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ partitionImpl.LoopInvariant arr first last last last
Tactic:
apply partitionImpl.LoopInvariant.intro
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k < last → arr[k] < arr[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k < last → arr[k] < arr[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]
Tactic:
. intro k lk kl
  exact (Nat.lt_irrefl k (Nat.lt_trans kl lk)).elim
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]
Tactic:
. intro k lk kl
  exact (Nat.lt_irrefl k (Nat.lt_of_le_of_lt kl lk)).elim
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]
Tactic:
. intro ll
  exact (Nat.lt_irrefl last ll).elim
State after:
no goals

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k < last → arr[k] < arr[first]
Tactic:
intro k lk kl
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
k : Fin n
lk : last < k
kl : k < last
⊢ arr[k] < arr[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
k : Fin n
lk : last < k
kl : k < last
⊢ arr[k] < arr[first]
Tactic:
exact (Nat.lt_irrefl k (Nat.lt_trans kl lk)).elim
State after:
no goals

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ ∀ (k : Fin n), last < k → k ≤ last → ¬arr[k] < arr[first]
Tactic:
intro k lk kl
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
k : Fin n
lk : last < k
kl : k ≤ last
⊢ ¬arr[k] < arr[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
k : Fin n
lk : last < k
kl : k ≤ last
⊢ ¬arr[k] < arr[first]
Tactic:
exact (Nat.lt_irrefl k (Nat.lt_of_le_of_lt kl lk)).elim
State after:
no goals

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ last < last → arr[last] < arr[first]
Tactic:
intro ll
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
ll : last < last
⊢ arr[last] < arr[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
ll : last < last
⊢ arr[last] < arr[first]
Tactic:
exact (Nat.lt_irrefl last ll).elim
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
⊢ partitionImpl arr first last last fl ⋯ = afterLoop
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk : first ≤ k
km : ↑k < ↑mid.val
⊢ swapped[k] < arr[first]
Tactic:
cases Nat.eq_or_lt_of_le fk with
| inl fk =>
  have : swapped[k] = swapped[first] := by
    simp [Fin.eq_of_val_eq fk]
  rw [this]
  have : swapped[first] = arr'[mid.val] := by
    apply Vec.get_swap_left
  rw [this, ←first_eq]
  exact inv.3 (Fin.eq_of_val_eq fk ▸ km)
| inr fk =>
  have : swapped[k] = arr'[k] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt fk
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt km
  rw [this, ←first_eq]
  exact inv.1 k fk km
State after:
no goals

State before:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
⊢ swapped[k] < arr[first]
Tactic:
have : swapped[k] = swapped[first] := by
  simp [Fin.eq_of_val_eq fk]
State after:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this : swapped[k] = swapped[first]
⊢ swapped[k] < arr[first]

State before:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this : swapped[k] = swapped[first]
⊢ swapped[k] < arr[first]
Tactic:
rw [this]
State after:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this : swapped[k] = swapped[first]
⊢ swapped[first] < arr[first]

State before:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this : swapped[k] = swapped[first]
⊢ swapped[first] < arr[first]
Tactic:
have : swapped[first] = arr'[mid.val] := by
  apply Vec.get_swap_left
State after:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝³ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝³⟩
this✝² : result.fst = mid
this✝¹ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this✝ : swapped[k] = swapped[first]
this : swapped[first] = arr'[mid.val]
⊢ swapped[first] < arr[first]

State before:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝³ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝³⟩
this✝² : result.fst = mid
this✝¹ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this✝ : swapped[k] = swapped[first]
this : swapped[first] = arr'[mid.val]
⊢ swapped[first] < arr[first]
Tactic:
rw [this, ←first_eq]
State after:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝³ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝³⟩
this✝² : result.fst = mid
this✝¹ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this✝ : swapped[k] = swapped[first]
this : swapped[first] = arr'[mid.val]
⊢ arr'[mid.val] < arr'[first]

State before:
case inl
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝³ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝³⟩
this✝² : result.fst = mid
this✝¹ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this✝ : swapped[k] = swapped[first]
this : swapped[first] = arr'[mid.val]
⊢ arr'[mid.val] < arr'[first]
Tactic:
exact inv.3 (Fin.eq_of_val_eq fk ▸ km)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
⊢ swapped[k] = swapped[first]
Tactic:
simp [Fin.eq_of_val_eq fk]
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first = ↑k
this : swapped[k] = swapped[first]
⊢ swapped[first] = arr'[mid.val]
Tactic:
apply Vec.get_swap_left
State after:
no goals

State before:
case inr
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ swapped[k] < arr[first]
Tactic:
have : swapped[k] = arr'[k] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt fk
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt km
State after:
case inr
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
this : swapped[k] = arr'[k]
⊢ swapped[k] < arr[first]

State before:
case inr
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
this : swapped[k] = arr'[k]
⊢ swapped[k] < arr[first]
Tactic:
rw [this, ←first_eq]
State after:
case inr
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
this : swapped[k] = arr'[k]
⊢ arr'[k] < arr'[first]

State before:
case inr
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
this : swapped[k] = arr'[k]
⊢ arr'[k] < arr'[first]
Tactic:
exact inv.1 k fk km
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ swapped[k] = arr'[k]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ first

case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ ⟨↑mid.val, this✝¹⟩

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ first

case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt fk
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ ⟨↑mid.val, this✝¹⟩

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt km
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ first
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ ¬↑k = ↑first

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ ¬↑k = ↑first
Tactic:
exact Nat.ne_of_gt fk
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
k : Fin n
fk✝ : first ≤ k
km : ↑k < ↑mid.val
fk : ↑first < ↑k
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩
Tactic:
exact Nat.ne_of_lt km
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
⊢ swapped[mid.val] = arr[first]
Tactic:
have : swapped[mid.val] = arr'[first] := by
  apply Vec.get_swap_right
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
this : swapped[mid.val] = arr'[first]
⊢ swapped[mid.val] = arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
this : swapped[mid.val] = arr'[first]
⊢ swapped[mid.val] = arr[first]
Tactic:
rw [this]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
this : swapped[mid.val] = arr'[first]
⊢ arr'[first] = arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
this : swapped[mid.val] = arr'[first]
⊢ arr'[first] = arr[first]
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
⊢ swapped[mid.val] = arr'[first]
Tactic:
apply Vec.get_swap_right
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬swapped[k] < arr[first]
Tactic:
have : swapped[k] = arr'[k] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt mid.property.1 mk)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt mk
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
this : swapped[k] = arr'[k]
⊢ ¬swapped[k] < arr[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
this : swapped[k] = arr'[k]
⊢ ¬swapped[k] < arr[first]
Tactic:
rw [this, ←first_eq]
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
this : swapped[k] = arr'[k]
⊢ ¬arr'[k] < arr'[first]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝² : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝²⟩
this✝¹ : result.fst = mid
this✝ : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
this : swapped[k] = arr'[k]
⊢ ¬arr'[k] < arr'[first]
Tactic:
exact inv.2 k mk kl
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ swapped[k] = arr'[k]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ first

case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ first

case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt mid.property.1 mk)
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt mk
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ first
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑first

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑first
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt mid.property.1 mk)
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩
Tactic:
exact Nat.ne_of_gt mk
State after:
no goals

State before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]
Tactic:
simp [*]
State after:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]

State before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
Tactic:
apply p₁
State after:
no goals

State before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first] ∧ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
apply And.intro
State after:
case right.left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first]

case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
case right.left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first]

case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
. simp [*]
State after:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]

State before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
. simp [*]
  apply p₃
State after:
no goals

State before:
case right.left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first]
Tactic:
simp [*]
State after:
no goals

State before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
simp [*]
State after:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]

State before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
Tactic:
apply p₃
State after:
no goals