Theorem: permuted_map_index (QuickSortInLean/Permutation.lean)

State before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
⊢ arr1[k] = arr2[p.to_map k]
Tactic:
induction p generalizing k with
| refl => simp [permuted.to_map]
| step i j fi ij jl p ih =>
  simp [permuted.to_map]
  rw [←ih]
  split
  case step.inl ki => simp [ki, Vec.get_swap_right]
  case step.inr nki =>
    split
    case inl kj => simp [kj, Vec.get_swap_left]
    case inr nkj => rw [Vec.get_swap_neq _ i j k nki nkj]
State after:
no goals

State before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ : Vec α✝ n
k : Fin n
⊢ arr✝[k] = arr✝[permuted.refl.to_map k]
Tactic:
simp [permuted.to_map]
State after:
no goals

State before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
⊢ arr✝[k] = arr'✝[(permuted.step i j fi ij jl p).to_map k]
Tactic:
simp [permuted.to_map]
State after:
case step
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
⊢ arr✝[k] = arr'✝[p.to_map (if k = i then j else if k = j then i else k)]

State before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
⊢ arr✝[k] = arr'✝[p.to_map (if k = i then j else if k = j then i else k)]
Tactic:
rw [←ih]
State after:
case step
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
⊢ arr✝[k] = (arr✝.swap i j)[if k = i then j else if k = j then i else k]

State before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
⊢ arr✝[k] = (arr✝.swap i j)[if k = i then j else if k = j then i else k]
Tactic:
split
State after:
case step.inl
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
h✝ : k = i
⊢ arr✝[k] = (arr✝.swap i j)[j]

case step.inr
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
h✝ : ¬k = i
⊢ arr✝[k] = (arr✝.swap i j)[if k = j then i else k]

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
ki : k = i
⊢ arr✝[k] = (arr✝.swap i j)[j]
Tactic:
case step.inl ki => simp [ki, Vec.get_swap_right]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
⊢ arr✝[k] = (arr✝.swap i j)[if k = j then i else k]
Tactic:
case step.inr nki =>
  split
  case inl kj => simp [kj, Vec.get_swap_left]
  case inr nkj => rw [Vec.get_swap_neq _ i j k nki nkj]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
ki : k = i
⊢ arr✝[k] = (arr✝.swap i j)[j]
Tactic:
simp [ki, Vec.get_swap_right]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
⊢ arr✝[k] = (arr✝.swap i j)[if k = j then i else k]
Tactic:
split
State after:
case inl
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
h✝ : k = j
⊢ arr✝[k] = (arr✝.swap i j)[i]

case inr
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
h✝ : ¬k = j
⊢ arr✝[k] = (arr✝.swap i j)[k]

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
kj : k = j
⊢ arr✝[k] = (arr✝.swap i j)[i]
Tactic:
case inl kj => simp [kj, Vec.get_swap_left]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
nkj : ¬k = j
⊢ arr✝[k] = (arr✝.swap i j)[k]
Tactic:
case inr nkj => rw [Vec.get_swap_neq _ i j k nki nkj]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
kj : k = j
⊢ arr✝[k] = (arr✝.swap i j)[i]
Tactic:
simp [kj, Vec.get_swap_left]
State after:
no goals

State before:
n first last : Nat
α✝ : Type
arr1 arr2 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 : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
nkj : ¬k = j
⊢ arr✝[k] = (arr✝.swap i j)[k]
Tactic:
rw [Vec.get_swap_neq _ i j k nki nkj]
State after:
no goals