Theorem: quickSort'_map_index_invertible (QuickSortInLean/QuickSortPermutation.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]
Tactic:
let p := quickSort'_permuted arr
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]
Tactic:
exists p.to_map
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
apply And.intro
State after:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]

State before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
. exact permuted_map_invertible p
State after:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]

State before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
. exact permuted_map_index p
State after:
no goals

State before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map
Tactic:
exact permuted_map_invertible p
State after:
no goals

State before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
exact permuted_map_index p
State after:
no goals