Theorem: permuted_map_index_invertible (QuickSortInLean/Permutation.lean)

State before:
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = arr'[f i]
Tactic:
exists p.to_map
State after:
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]

State before:
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]
Tactic:
apply And.intro
State after:
case left
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ invertible p.to_map

case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]

State before:
case left
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ invertible p.to_map

case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]
Tactic:
. exact permuted_map_invertible p
State after:
case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]

State before:
case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]
Tactic:
. intro i
  exact permuted_map_index p i
State after:
no goals

State before:
case left
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ invertible p.to_map
Tactic:
exact permuted_map_invertible p
State after:
no goals

State before:
case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
⊢ ∀ (i : Fin n), arr[i] = arr'[p.to_map i]
Tactic:
intro i
State after:
case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
i : Fin n
⊢ arr[i] = arr'[p.to_map i]

State before:
case right
α : Type
n first last : Nat
arr arr' : Vec α n
p : permuted n first last arr arr'
i : Fin n
⊢ arr[i] = arr'[p.to_map i]
Tactic:
exact permuted_map_index p i
State after:
no goals