Theorem: partitionImpl.loop_invariant (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j last : Fin n
fi : first ≤ i
ij : i ≤ j
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi ij = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
induction arr, first, i, j, fi, ij using partitionImpl.induct' with
| base arr first i j fi _ h =>
  revert result
  simp [*]
  have : i = first := Fin.eq_of_val_eq (Nat.le_antisymm (Nat.le_of_not_lt h) fi)
  exact this ▸ inv
| step_lt arr first i j _ _ fi _ lt _ ih =>
  have inv : LoopInvariant arr first i.prev j last := by
    apply LoopInvariant.intro
    . intro k ik kj
      have ik : i.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ik
      cases Nat.eq_or_lt_of_le ik with
      | inl ik =>
        simp [Fin.eq_of_val_eq ik] at lt
        exact lt
      | inr ik => exact inv.1 k ik kj
    . exact inv.2
    . intro ij
      have ij : i.val ≤ j.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ij
      cases Nat.eq_or_lt_of_le ij with
      | inl ij =>
        simp [Fin.eq_of_val_eq ij.symm]
        assumption
      | inr ij => exact inv.3 ij
  simp [*] at eq
  apply ih inv result eq
| step_ge arr first i j _ ij fi _ _ _ ih =>
  let swapped := arr.swap i j
  have sf : swapped[first] = arr[first] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt fi
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
  let result := partitionImpl swapped first i.prev j.prev (by assumption) (by assumption)
  subst eq
  simp [*]
  have inv : LoopInvariant swapped first i.prev j.prev last := by
    apply LoopInvariant.intro
    . intro k ik kj
      have ik : i.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ik
      cases Nat.eq_or_lt_of_le ik with
      | inl ik =>
        have : swapped[k] = arr[j] := by
          simp [Fin.eq_of_val_eq ik.symm]
          apply Vec.get_swap_left
        rw [this, sf]
        exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
      | inr ik =>
        have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
        have : swapped[k] = arr[k] := by
          apply Vec.get_swap_neq
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt ik
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_lt kj
        rw [this, sf]
        exact inv.1 k ik kj
    . intro k jk kl
      have jk : j.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
        exact jk
      cases Nat.eq_or_lt_of_le jk with
      | inl jk =>
        have : swapped[k] = arr[i] := by
          simp [Fin.eq_of_val_eq jk.symm]
          apply Vec.get_swap_right
        rw [this, sf]
        assumption
      | inr jk =>
        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 ij jk)
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt jk
        rw [this, sf]
        exact inv.2 k jk kl
    . intro ij
      have : j.val - 1 < j.val := by
        show j.val - 1 + 1 ≤ j.val
        rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
        apply Nat.le_refl
      have ij : i.val ≤ j.val - 1 := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ij
      cases Nat.eq_or_lt_of_le ij with
      | inl ij =>
        have : swapped[j.prev] = arr[j] := by
          simp [ij.symm, Fin.prev]
          apply Vec.get_swap_left
        rw [this, sf]
        have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
        exact inv.3 this
      | inr ij =>
        have : swapped[j.prev] = arr[j.prev] := by
          apply Vec.get_swap_neq
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt ij
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_lt (by assumption)
        rw [this, sf]
        apply inv.1 j.prev ij (by assumption)
  exact ih inv result (by rfl)
State after:
no goals

State before:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi ij✝ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
revert result
State after:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
    partitionImpl arr first i j fi ij✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last

State before:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
    partitionImpl arr first i j fi ij✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
simp [*]
State after:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ LoopInvariant arr first first j last

State before:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ LoopInvariant arr first first j last
Tactic:
have : i = first := Fin.eq_of_val_eq (Nat.le_antisymm (Nat.le_of_not_lt h) fi)
State after:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
this : i = first
⊢ LoopInvariant arr first first j last

State before:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
this : i = first
⊢ LoopInvariant arr first first j last
Tactic:
exact this ▸ inv
State after:
no goals

State before:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
have inv : LoopInvariant arr first i.prev j last := by
  apply LoopInvariant.intro
  . intro k ik kj
    have ik : i.val ≤ k.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ik
    cases Nat.eq_or_lt_of_le ik with
    | inl ik =>
      simp [Fin.eq_of_val_eq ik] at lt
      exact lt
    | inr ik => exact inv.1 k ik kj
  . exact inv.2
  . intro ij
    have ij : i.val ≤ j.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ij
    cases Nat.eq_or_lt_of_le ij with
    | inl ij =>
      simp [Fin.eq_of_val_eq ij.symm]
      assumption
    | inr ij => exact inv.3 ij
State after:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
inv : LoopInvariant arr first i.prev j last
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last

State before:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
inv : LoopInvariant arr first i.prev j last
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
simp [*] at eq
State after:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
inv : LoopInvariant arr first i.prev j last
eq : partitionImpl arr first i.prev j ⋯ ⋯ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last

State before:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
inv : LoopInvariant arr first i.prev j last
eq : partitionImpl arr first i.prev j ⋯ ⋯ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
apply ih inv result eq
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ LoopInvariant arr first i.prev j last
Tactic:
apply LoopInvariant.intro
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), i.prev < k → k < j → arr[k] < arr[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), i.prev < k → k < j → arr[k] < arr[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
. intro k ik kj
  have ik : i.val ≤ k.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ik
  cases Nat.eq_or_lt_of_le ik with
  | inl ik =>
    simp [Fin.eq_of_val_eq ik] at lt
    exact lt
  | inr ik => exact inv.1 k ik kj
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
. exact inv.2
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
. intro ij
  have ij : i.val ≤ j.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ij
  cases Nat.eq_or_lt_of_le ij with
  | inl ij =>
    simp [Fin.eq_of_val_eq ij.symm]
    assumption
  | inr ij => exact inv.3 ij
State after:
no goals

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), i.prev < k → k < j → arr[k] < arr[first]
Tactic:
intro k ik kj
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik : i.prev < k
kj : k < j
⊢ arr[k] < arr[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik : i.prev < k
kj : k < j
⊢ arr[k] < arr[first]
Tactic:
have ik : i.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ik
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝ : i.prev < k
kj : k < j
ik : ↑i ≤ ↑k
⊢ arr[k] < arr[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝ : i.prev < k
kj : k < j
ik : ↑i ≤ ↑k
⊢ arr[k] < arr[first]
Tactic:
cases Nat.eq_or_lt_of_le ik with
| inl ik =>
  simp [Fin.eq_of_val_eq ik] at lt
  exact lt
| inr ik => exact inv.1 k ik kj
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i ≤ ↑k
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k
Tactic:
exact ik
State after:
no goals

State before:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ arr[k] < arr[first]
Tactic:
simp [Fin.eq_of_val_eq ik] at lt
State after:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
lt : arr[k] < arr[first]
⊢ arr[k] < arr[first]

State before:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
lt : arr[k] < arr[first]
⊢ arr[k] < arr[first]
Tactic:
exact lt
State after:
no goals

State before:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
⊢ arr[k] < arr[first]
Tactic:
exact inv.1 k ik kj
State after:
no goals

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]
Tactic:
exact inv.2
State after:
no goals

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
intro ij
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ arr[j] < arr[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ arr[j] < arr[first]
Tactic:
have ij : i.val ≤ j.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ij
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝¹ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝¹ = result
ij✝ : i.prev < j
ij : ↑i ≤ ↑j
⊢ arr[j] < arr[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝¹ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝¹ = result
ij✝ : i.prev < j
ij : ↑i ≤ ↑j
⊢ arr[j] < arr[first]
Tactic:
cases Nat.eq_or_lt_of_le ij with
| inl ij =>
  simp [Fin.eq_of_val_eq ij.symm]
  assumption
| inr ij => exact inv.3 ij
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i ≤ ↑j
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j
Tactic:
exact ij
State after:
no goals

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[j] < arr[first]
Tactic:
simp [Fin.eq_of_val_eq ij.symm]
State after:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[i] < arr[first]

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[i] < arr[first]
Tactic:
assumption
State after:
no goals

State before:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i < ↑j
⊢ arr[j] < arr[first]
Tactic:
exact inv.3 ij
State after:
no goals

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
let swapped := arr.swap i j
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
have sf : swapped[first] = arr[first] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt fi
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
let result := partitionImpl swapped first i.prev j.prev (by assumption) (by assumption)
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result✝ : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result✝
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant result✝.snd first first ⟨↑result✝.fst.val, ⋯⟩ last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result✝ : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result✝
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant result✝.snd first first ⟨↑result✝.fst.val, ⋯⟩ last
Tactic:
subst eq
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl arr first i j fi✝ ij).snd first first ⟨↑(partitionImpl arr first i j fi✝ ij).fst.val, ⋯⟩
    last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl arr first i j fi✝ ij).snd first first ⟨↑(partitionImpl arr first i j fi✝ ij).fst.val, ⋯⟩
    last
Tactic:
simp [*]
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last
Tactic:
have inv : LoopInvariant swapped first i.prev j.prev last := by
  apply LoopInvariant.intro
  . intro k ik kj
    have ik : i.val ≤ k.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ik
    cases Nat.eq_or_lt_of_le ik with
    | inl ik =>
      have : swapped[k] = arr[j] := by
        simp [Fin.eq_of_val_eq ik.symm]
        apply Vec.get_swap_left
      rw [this, sf]
      exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
    | inr ik =>
      have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
      have : swapped[k] = arr[k] := by
        apply Vec.get_swap_neq
        . apply Fin.ne_of_val_ne
          exact Nat.ne_of_gt ik
        . apply Fin.ne_of_val_ne
          exact Nat.ne_of_lt kj
      rw [this, sf]
      exact inv.1 k ik kj
  . intro k jk kl
    have jk : j.val ≤ k.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
      exact jk
    cases Nat.eq_or_lt_of_le jk with
    | inl jk =>
      have : swapped[k] = arr[i] := by
        simp [Fin.eq_of_val_eq jk.symm]
        apply Vec.get_swap_right
      rw [this, sf]
      assumption
    | inr jk =>
      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 ij jk)
        . apply Fin.ne_of_val_ne
          exact Nat.ne_of_gt jk
      rw [this, sf]
      exact inv.2 k jk kl
  . intro ij
    have : j.val - 1 < j.val := by
      show j.val - 1 + 1 ≤ j.val
      rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
      apply Nat.le_refl
    have ij : i.val ≤ j.val - 1 := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ij
    cases Nat.eq_or_lt_of_le ij with
    | inl ij =>
      have : swapped[j.prev] = arr[j] := by
        simp [ij.symm, Fin.prev]
        apply Vec.get_swap_left
      rw [this, sf]
      have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
      exact inv.3 this
    | inr ij =>
      have : swapped[j.prev] = arr[j.prev] := by
        apply Vec.get_swap_neq
        . apply Fin.ne_of_val_ne
          exact Nat.ne_of_gt ij
        . apply Fin.ne_of_val_ne
          exact Nat.ne_of_lt (by assumption)
      rw [this, sf]
      apply inv.1 j.prev ij (by assumption)
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
inv : LoopInvariant swapped first i.prev j.prev last
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
inv : LoopInvariant swapped first i.prev j.prev last
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last
Tactic:
exact ih inv result (by rfl)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ swapped[first] = arr[first]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt fi
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑i

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑i
Tactic:
exact Nat.ne_of_lt fi
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑j

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑j
Tactic:
exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ first ≤ i.prev
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ i.prev ≤ j.prev
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant swapped first i.prev j.prev last
Tactic:
apply LoopInvariant.intro
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), i.prev < k → k < j.prev → swapped[k] < swapped[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), i.prev < k → k < j.prev → swapped[k] < swapped[first]

case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]
Tactic:
. intro k ik kj
  have ik : i.val ≤ k.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ik
  cases Nat.eq_or_lt_of_le ik with
  | inl ik =>
    have : swapped[k] = arr[j] := by
      simp [Fin.eq_of_val_eq ik.symm]
      apply Vec.get_swap_left
    rw [this, sf]
    exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
  | inr ik =>
    have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
    have : swapped[k] = arr[k] := by
      apply Vec.get_swap_neq
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_gt ik
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_lt kj
    rw [this, sf]
    exact inv.1 k ik kj
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]

case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]
Tactic:
. intro k jk kl
  have jk : j.val ≤ k.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
    exact jk
  cases Nat.eq_or_lt_of_le jk with
  | inl jk =>
    have : swapped[k] = arr[i] := by
      simp [Fin.eq_of_val_eq jk.symm]
      apply Vec.get_swap_right
    rw [this, sf]
    assumption
  | inr jk =>
    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 ij jk)
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_gt jk
    rw [this, sf]
    exact inv.2 k jk kl
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]
Tactic:
. intro ij
  have : j.val - 1 < j.val := by
    show j.val - 1 + 1 ≤ j.val
    rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
    apply Nat.le_refl
  have ij : i.val ≤ j.val - 1 := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ij
  cases Nat.eq_or_lt_of_le ij with
  | inl ij =>
    have : swapped[j.prev] = arr[j] := by
      simp [ij.symm, Fin.prev]
      apply Vec.get_swap_left
    rw [this, sf]
    have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
    exact inv.3 this
  | inr ij =>
    have : swapped[j.prev] = arr[j.prev] := by
      apply Vec.get_swap_neq
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_gt ij
      . apply Fin.ne_of_val_ne
        exact Nat.ne_of_lt (by assumption)
    rw [this, sf]
    apply inv.1 j.prev ij (by assumption)
State after:
no goals

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), i.prev < k → k < j.prev → swapped[k] < swapped[first]
Tactic:
intro k ik kj
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ swapped[k] < swapped[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ swapped[k] < swapped[first]
Tactic:
have ik : i.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ik
State after:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝ : i.prev < k
kj : k < j.prev
ik : ↑i ≤ ↑k
⊢ swapped[k] < swapped[first]

State before:
case inv₁
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝ : i.prev < k
kj : k < j.prev
ik : ↑i ≤ ↑k
⊢ swapped[k] < swapped[first]
Tactic:
cases Nat.eq_or_lt_of_le ik with
| inl ik =>
  have : swapped[k] = arr[j] := by
    simp [Fin.eq_of_val_eq ik.symm]
    apply Vec.get_swap_left
  rw [this, sf]
  exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
| inr ik =>
  have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
  have : swapped[k] = arr[k] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt ik
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt kj
  rw [this, sf]
  exact inv.1 k ik kj
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ ↑i ≤ ↑k
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k
Tactic:
exact ik
State after:
no goals

State before:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ swapped[k] < swapped[first]
Tactic:
have : swapped[k] = arr[j] := by
  simp [Fin.eq_of_val_eq ik.symm]
  apply Vec.get_swap_left
State after:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
this : swapped[k] = arr[j]
⊢ swapped[k] < swapped[first]

State before:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
this : swapped[k] = arr[j]
⊢ swapped[k] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
this : swapped[k] = arr[j]
⊢ arr[j] < arr[first]

State before:
case inv₁.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
this : swapped[k] = arr[j]
⊢ arr[j] < arr[first]
Tactic:
exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ swapped[k] = arr[j]
Tactic:
simp [Fin.eq_of_val_eq ik.symm]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ swapped[i] = arr[j]

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ swapped[i] = arr[j]
Tactic:
apply Vec.get_swap_left
State after:
no goals

State before:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
⊢ swapped[k] < swapped[first]
Tactic:
have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
State after:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] < swapped[first]

State before:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] < swapped[first]
Tactic:
have : swapped[k] = arr[k] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt ik
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt kj
State after:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ swapped[k] < swapped[first]

State before:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ swapped[k] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ arr[k] < arr[first]

State before:
case inv₁.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ arr[k] < arr[first]
Tactic:
exact inv.1 k ik kj
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] = arr[k]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt ik
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt kj
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑i

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_gt ik
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑j

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_lt kj
State after:
no goals

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]
Tactic:
intro k jk kl
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ¬swapped[k] < swapped[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ¬swapped[k] < swapped[first]
Tactic:
have jk : j.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
  exact jk
State after:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝ : j.prev < k
kl : k ≤ last
jk : ↑j ≤ ↑k
⊢ ¬swapped[k] < swapped[first]

State before:
case inv₂
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝ : j.prev < k
kl : k ≤ last
jk : ↑j ≤ ↑k
⊢ ¬swapped[k] < swapped[first]
Tactic:
cases Nat.eq_or_lt_of_le jk with
| inl jk =>
  have : swapped[k] = arr[i] := by
    simp [Fin.eq_of_val_eq jk.symm]
    apply Vec.get_swap_right
  rw [this, sf]
  assumption
| inr jk =>
  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 ij jk)
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt jk
  rw [this, sf]
  exact inv.2 k jk kl
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ↑j ≤ ↑k
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ↑j - Nat.succ 0 + Nat.succ 0 ≤ ↑k

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ↑j - Nat.succ 0 + Nat.succ 0 ≤ ↑k
Tactic:
exact jk
State after:
no goals

State before:
case inv₂.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
⊢ ¬swapped[k] < swapped[first]
Tactic:
have : swapped[k] = arr[i] := by
  simp [Fin.eq_of_val_eq jk.symm]
  apply Vec.get_swap_right
State after:
case inv₂.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
this : swapped[k] = arr[i]
⊢ ¬swapped[k] < swapped[first]

State before:
case inv₂.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
this : swapped[k] = arr[i]
⊢ ¬swapped[k] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₂.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
this : swapped[k] = arr[i]
⊢ ¬arr[i] < arr[first]

State before:
case inv₂.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
this : swapped[k] = arr[i]
⊢ ¬arr[i] < arr[first]
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
⊢ swapped[k] = arr[i]
Tactic:
simp [Fin.eq_of_val_eq jk.symm]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
⊢ swapped[j] = arr[i]

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j = ↑k
⊢ swapped[j] = arr[i]
Tactic:
apply Vec.get_swap_right
State after:
no goals

State before:
case inv₂.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ ¬swapped[k] < swapped[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 ij jk)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt jk
State after:
case inv₂.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
this : swapped[k] = arr[k]
⊢ ¬swapped[k] < swapped[first]

State before:
case inv₂.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
this : swapped[k] = arr[k]
⊢ ¬swapped[k] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₂.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
this : swapped[k] = arr[k]
⊢ ¬arr[k] < arr[first]

State before:
case inv₂.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
this : swapped[k] = arr[k]
⊢ ¬arr[k] < arr[first]
Tactic:
exact inv.2 k jk kl
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ swapped[k] = arr[k]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ j

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt ij jk)
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ j

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt jk
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ ¬↑k = ↑i

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt ij jk)
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ k ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ ¬↑k = ↑j

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
jk✝¹ : j.prev < k
kl : k ≤ last
jk✝ : ↑j ≤ ↑k
jk : ↑j < ↑k
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_gt jk
State after:
no goals

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ i.prev < j.prev → swapped[j.prev] < swapped[first]
Tactic:
intro ij
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ swapped[j.prev] < swapped[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ swapped[j.prev] < swapped[first]
Tactic:
have : j.val - 1 < j.val := by
  show j.val - 1 + 1 ≤ j.val
  rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
  apply Nat.le_refl
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
this : ↑j - 1 < ↑j
⊢ swapped[j.prev] < swapped[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
this : ↑j - 1 < ↑j
⊢ swapped[j.prev] < swapped[first]
Tactic:
have ij : i.val ≤ j.val - 1 := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ij
State after:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝¹ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij : ↑i ≤ ↑j - 1
⊢ swapped[j.prev] < swapped[first]

State before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝¹ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij : ↑i ≤ ↑j - 1
⊢ swapped[j.prev] < swapped[first]
Tactic:
cases Nat.eq_or_lt_of_le ij with
| inl ij =>
  have : swapped[j.prev] = arr[j] := by
    simp [ij.symm, Fin.prev]
    apply Vec.get_swap_left
  rw [this, sf]
  have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
  exact inv.3 this
| inr ij =>
  have : swapped[j.prev] = arr[j.prev] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt ij
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt (by assumption)
  rw [this, sf]
  apply inv.1 j.prev ij (by assumption)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑j - 1 < ↑j
Tactic:
show j.val - 1 + 1 ≤ j.val
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑j - 1 + 1 ≤ ↑j

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑j - 1 + 1 ≤ ↑j
Tactic:
rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑j ≤ ↑j

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑j ≤ ↑j
Tactic:
apply Nat.le_refl
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
⊢ ↑i ≤ ↑j
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
this : ↑j - 1 < ↑j
⊢ ↑i ≤ ↑j - 1
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
this : ↑j - 1 < ↑j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j - 1

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij : i.prev < j.prev
this : ↑j - 1 < ↑j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j - 1
Tactic:
exact ij
State after:
no goals

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
⊢ swapped[j.prev] < swapped[first]
Tactic:
have : swapped[j.prev] = arr[j] := by
  simp [ij.symm, Fin.prev]
  apply Vec.get_swap_left
State after:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ swapped[j.prev] < swapped[first]

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ swapped[j.prev] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ arr[j] < arr[first]

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ arr[j] < arr[first]
Tactic:
have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
State after:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝¹ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this✝ : swapped[j.prev] = arr[j]
this : i < j
⊢ arr[j] < arr[first]

State before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝¹ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this✝ : swapped[j.prev] = arr[j]
this : i < j
⊢ arr[j] < arr[first]
Tactic:
exact inv.3 this
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
⊢ swapped[j.prev] = arr[j]
Tactic:
simp [ij.symm, Fin.prev]
State after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
⊢ swapped[i] = arr[j]

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
⊢ swapped[i] = arr[j]
Tactic:
apply Vec.get_swap_left
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ ↑i ≤ ↑j - 1
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ ↑j - 1 < ↑j
Tactic:
assumption
State after:
no goals

State before:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ swapped[j.prev] < swapped[first]
Tactic:
have : swapped[j.prev] = arr[j.prev] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt ij
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (by assumption)
State after:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ swapped[j.prev] < swapped[first]

State before:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ swapped[j.prev] < swapped[first]
Tactic:
rw [this, sf]
State after:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ arr[j.prev] < arr[first]

State before:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ arr[j.prev] < arr[first]
Tactic:
apply inv.1 j.prev ij (by assumption)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ swapped[j.prev] = arr[j.prev]
Tactic:
apply Vec.get_swap_neq
State after:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt ij
State after:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (by assumption)
State after:
no goals

State before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑i

State before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑i
Tactic:
exact Nat.ne_of_gt ij
State after:
no goals

State before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑j

State before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑j
Tactic:
exact Nat.ne_of_lt (by assumption)
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ↑j.prev < ↑j
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ j.prev < j
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
inv : LoopInvariant swapped first i.prev j.prev last
⊢ partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result
Tactic:
rfl
State after:
no goals