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

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
⊢ (partitionImpl arr first i j fi ij).snd[first] = arr[first]
Tactic:
induction arr, first, i, j, fi, ij using partitionImpl.induct' with
| base => simp [*]
| step_lt => simp [*]
| step_ge arr first i j _ ij fi =>
  simp [*]
  have fj : first < j := Nat.lt_of_lt_of_le fi ij
  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 fj
State after:
no goals

State before:
case base
α : Type
inst✝ : Ord α
n : Nat
first i j : Fin n
arr✝ : Vec α n
first✝ i✝ j✝ : Fin n
fi✝ : first✝ ≤ i✝
ij✝ : i✝ ≤ j✝
x✝ : ¬first✝ < i✝
⊢ (partitionImpl arr✝ first✝ i✝ j✝ fi✝ ij✝).snd[first✝] = arr✝[first✝]
Tactic:
simp [*]
State after:
no goals

State before:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first i j : Fin n
arr✝ : Vec α n
first✝ i✝ j✝ : Fin n
fi✝ : first✝ ≤ i✝
ij✝ : i✝ ≤ j✝
x✝³ : first✝ < i✝
x✝² : ↑first✝ ≤ ↑i✝ - 1
x✝¹ : arr✝[i✝] < arr✝[first✝]
x✝ : ↑i✝ - 1 ≤ ↑j✝
ih✝ : (partitionImpl arr✝ first✝ i✝.prev j✝ x✝² x✝).snd[first✝] = arr✝[first✝]
⊢ (partitionImpl arr✝ first✝ i✝ j✝ fi✝ ij✝).snd[first✝] = arr✝[first✝]
Tactic:
simp [*]
State after:
no goals

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (partitionImpl arr first i j fi✝ ij).snd[first] = arr[first]
Tactic:
simp [*]
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (arr.swap i j)[first] = arr[first]

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (arr.swap i j)[first] = arr[first]
Tactic:
have fj : first < j := Nat.lt_of_lt_of_le fi ij
State after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ (arr.swap i j)[first] = arr[first]

State before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ (arr.swap i j)[first] = arr[first]
Tactic:
apply Vec.get_swap_neq
State after:
case step_ge.ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ i

case step_ge.kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ j

State before:
case step_ge.ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ i

case step_ge.kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt fi
State after:
case step_ge.kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ j

State before:
case step_ge.kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt fj
State after:
no goals

State before:
case step_ge.ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case step_ge.ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ ¬↑first = ↑i

State before:
case step_ge.ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ ¬↑first = ↑i
Tactic:
exact Nat.ne_of_lt fi
State after:
no goals

State before:
case step_ge.kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ first ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case step_ge.kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ ¬↑first = ↑j

State before:
case step_ge.kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ ¬↑first = ↑j
Tactic:
exact Nat.ne_of_lt fj
State after:
no goals