Theorem: partitionImpl.loop_invariant
Proof 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)
Proof 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