Theorem: permuted_map_index_in_range_inv (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
⊢ ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑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', ⟨index, fk', kl'⟩⟩ := ih k fk kl
  let k'' := if k' = i then j else if k' = j then i else k'
  exists k''
  have : (if k'' = i then j else if k'' = j then i else k'') = k' := by
    match decEq k' i, decEq k' j with
    | isTrue ki, _ => simp [k'', ki]
    | _, isTrue kj => simp [k'', kj]
    | isFalse ki, isFalse kj => simp [k'',ki, kj]
  rw [this]
  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 ⟨index, 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
⊢ ∃ k', permuted.refl.to_map k' = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ ∃ k', (permuted.step i j fi ij jl p).to_map k' = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
let ⟨k', ⟨index, fk', kl'⟩⟩ := ih k 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
⊢ ∃ k', p.to_map (if k' = i then j else if k' = j then i else k') = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
exists 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := 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'') = k ∧ first ≤ ↑k'' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := 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'') = k ∧ first ≤ ↑k'' ∧ ↑k'' ≤ last
Tactic:
have : (if k'' = i then j else if k'' = j then i else k'') = k' := by
  match decEq k' i, decEq k' j with
  | isTrue ki, _ => simp [k'', ki]
  | _, isTrue kj => simp [k'', kj]
  | isFalse ki, isFalse kj => simp [k'',ki, kj]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
⊢ p.to_map (if k'' = i then j else if k'' = j then i else k'') = k ∧ first ≤ ↑k'' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
⊢ p.to_map (if k'' = i then j else if k'' = j then i else k'') = k ∧ first ≤ ↑k'' ∧ ↑k'' ≤ last
Tactic:
rw [this]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
⊢ p.to_map k' = k ∧ first ≤ ↑k'' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
⊢ p.to_map k' = k ∧ first ≤ ↑k'' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this✝ : (if k'' = i then j else if k'' = j then i else k'') = k'
this : first ≤ ↑k'' ∧ ↑k'' ≤ last
⊢ p.to_map k' = k ∧ first ≤ ↑k'' ∧ ↑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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this✝ : (if k'' = i then j else if k'' = j then i else k'') = k'
this : first ≤ ↑k'' ∧ ↑k'' ≤ last
⊢ p.to_map k' = k ∧ first ≤ ↑k'' ∧ ↑k'' ≤ last
Tactic:
exact ⟨index, 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
⊢ (if k'' = i then j else if k'' = j then i else k'') = k'
Tactic:
match decEq k' i, decEq k' j with
| isTrue ki, _ => simp [k'', ki]
| _, isTrue kj => simp [k'', kj]
| isFalse ki, isFalse kj => simp [k'',ki, kj]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
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)
⊢ (if k'' = i then j else if k'' = j then i else k'') = k'
Tactic:
simp [k'', ki]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
x✝ : Decidable (k' = i)
kj : k' = j
⊢ (if k'' = i then j else if k'' = j then i else k'') = k'
Tactic:
simp [k'', kj]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
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
⊢ (if k'' = i then j else if k'' = j then i else k'') = k'
Tactic:
simp [k'',ki, kj]
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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = 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 → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
ki : ¬k' = i
kj : ¬k' = j
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
exact ⟨fk', kl'⟩
State after:
no goals