Theorem: permuted_map_index_in_range (QuickSortInLean/Permutation.lean)

State before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
Tactic:
induction p generalizing k with
| refl => simp [permuted.to_map, fk, kl]
| step i j fi ij jl p ih =>
  simp [permuted.to_map]
  let k' := if k = i then j else if k = j then i else k
  have : first ≤ k'.val ∧ k'.val ≤ last := by
    match decEq k i, decEq k j with
    | isTrue ki, _ =>
      simp [k', ki]
      exact ⟨Nat.le_trans fi ij, jl⟩
    | isFalse ki, isTrue kj =>
      simp [k', ki]
      simp [kj]
      exact ⟨fi, Nat.le_trans ij jl⟩
    | isFalse ki, isFalse kj =>
      simp [k', ki, kj]
      exact ⟨fk, kl⟩
  exact ih k' this.1 this.2
State after:
no goals

State before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ : Vec α✝ n
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑(permuted.refl.to_map k) ∧ ↑(permuted.refl.to_map k) ≤ last
Tactic:
simp [permuted.to_map, fk, kl]
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑((permuted.step i j fi ij jl p).to_map k) ∧ ↑((permuted.step i j fi ij jl p).to_map k) ≤ last
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last
Tactic:
let k' := if k = i then j else if k = j then i else k
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last
Tactic:
have : first ≤ k'.val ∧ k'.val ≤ last := by
  match decEq k i, decEq k j with
  | isTrue ki, _ =>
    simp [k', ki]
    exact ⟨Nat.le_trans fi ij, jl⟩
  | isFalse ki, isTrue kj =>
    simp [k', ki]
    simp [kj]
    exact ⟨fi, Nat.le_trans ij jl⟩
  | isFalse ki, isFalse kj =>
    simp [k', ki, kj]
    exact ⟨fk, kl⟩
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
this : first ≤ ↑k' ∧ ↑k' ≤ last
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
this : first ≤ ↑k' ∧ ↑k' ≤ last
⊢ first ≤ ↑(p.to_map (if k = i then j else if k = j then i else k)) ∧
    ↑(p.to_map (if k = i then j else if k = j then i else k)) ≤ last
Tactic:
exact ih k' this.1 this.2
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
match decEq k i, decEq k j with
| isTrue ki, _ =>
  simp [k', ki]
  exact ⟨Nat.le_trans fi ij, jl⟩
| isFalse ki, isTrue kj =>
  simp [k', ki]
  simp [kj]
  exact ⟨fi, Nat.le_trans ij jl⟩
| isFalse ki, isFalse kj =>
  simp [k', ki, kj]
  exact ⟨fk, kl⟩
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : k = i
x✝ : Decidable (k = j)
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
simp [k', ki]
State after:
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : k = i
x✝ : Decidable (k = j)
⊢ first ≤ ↑j ∧ ↑j ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : k = i
x✝ : Decidable (k = j)
⊢ first ≤ ↑j ∧ ↑j ≤ last
Tactic:
exact ⟨Nat.le_trans fi ij, jl⟩
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : k = j
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
simp [k', ki]
State after:
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : k = j
⊢ first ≤ ↑(if k = j then i else k) ∧ ↑(if k = j then i else k) ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : k = j
⊢ first ≤ ↑(if k = j then i else k) ∧ ↑(if k = j then i else k) ≤ last
Tactic:
simp [kj]
State after:
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : k = j
⊢ first ≤ ↑i ∧ ↑i ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : k = j
⊢ first ≤ ↑i ∧ ↑i ≤ last
Tactic:
exact ⟨fi, Nat.le_trans ij jl⟩
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : ¬k = j
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
simp [k', ki, kj]
State after:
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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : ¬k = j
⊢ first ≤ ↑k ∧ ↑k ≤ last

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), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : ¬k = i
kj : ¬k = j
⊢ first ≤ ↑k ∧ ↑k ≤ last
Tactic:
exact ⟨fk, kl⟩
State after:
no goals