Theorem: permuted.get_gt (QuickSortInLean/Permutation.lean)

State before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
gt : last < ↑k
⊢ arr2[k] = arr1[k]
Tactic:
induction p with
| refl => rfl
| step i j fi ij jl p ih =>
  rw [ih]
  rw [Vec.get_swap_neq _ i j k]
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
State after:
no goals

State before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ : Vec α✝ n
⊢ arr✝[k] = arr✝[k]
Tactic:
rfl
State after:
no goals

State before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ arr'✝[k] = arr✝[k]
Tactic:
rw [ih]
State after:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]

State before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]
Tactic:
rw [Vec.get_swap_neq _ i j k]
State after:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j

State before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
State after:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j

State before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
State after:
no goals

State before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i
Tactic:
apply Fin.ne_of_val_ne
State after:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i

State before:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
State after:
no goals

State before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
apply Fin.ne_of_val_ne
State after:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j

State before:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
State after:
no goals