internlm/Lean-Github huggingface dataset:
Theorem: permuted_map_invertible
Proof state before:
case isFalse.isFalse
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
nfyj : ¬f' y = j
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
Tactic:
simp [nfyi, nfyj, permuted.to_map, h2, f]
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof state before:
case isFalse.isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
fyj : f' y = j
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
Tactic:
simp [nfyi, fyj, permuted.to_map, f]
Proof state after:
case isFalse.isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
fyj : f' y = j
⊢ p.to_map j = y
Theorem: permuted_map_invertible
Proof state before:
case isFalse.isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
fyj : f' y = j
⊢ p.to_map j = y
Tactic:
rw [←(congrArg p.to_map fyj), h2]
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof state before:
case isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
Tactic:
simp [fyi, f, permuted.to_map]
Proof state after:
case isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
⊢ p.to_map (if j = i then j else i) = y
Theorem: permuted_map_invertible
Proof state before:
case isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
⊢ p.to_map (if j = i then j else i) = y
Tactic:
have : (if j = i then j else i) = i := by simp
Proof state after:
case isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
this : (if j = i then j else i) = i
⊢ p.to_map (if j = i then j else i) = y
Theorem: permuted_map_invertible
Proof state before:
case isTrue
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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
this : (if j = i then j else i) = i
⊢ p.to_map (if j = i then j else i) = y
Tactic:
rw [this, ←(congrArg p.to_map fyi), h2]
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof 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 : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
fyi : f' y = i
⊢ (if j = i then j else i) = i
Tactic:
simp
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof 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)]
Theorem: permuted_map_index
Proof 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]
Proof 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]
Theorem: permuted_map_index
Proof 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
Proof 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]
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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
Proof 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]
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index_invertible
Proof 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
Proof 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]
Theorem: permuted_map_index_invertible
Proof 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
Proof 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]
Theorem: permuted_map_index_invertible
Proof 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
Proof 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]
Theorem: permuted_map_index_invertible
Proof 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
Proof state after:
no goals
Theorem: permuted_map_index_invertible
Proof 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
Proof state after:
no goals
Theorem: permuted_map_index_invertible
Proof 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
Proof 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]
Theorem: permuted_map_index_invertible
Proof 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
Proof state after:
no goals
Theorem: permuted_map_index_in_range
Proof 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
Proof state after:
no goals
Theorem: permuted_map_index_in_range
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_index_in_range
Proof 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]
Proof 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
Theorem: permuted_map_index_in_range
Proof 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
Proof 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
Theorem: permuted_map_index_in_range
Proof 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⟩
Proof 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
Theorem: permuted_map_index_in_range
Proof 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
Proof state after:
no goals
Theorem: permuted_map_index_in_range
Proof 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⟩
Proof state after:
no goals
Theorem: permuted_map_index_in_range
Proof 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]
Proof 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
Theorem: permuted_map_index_in_range
Proof 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⟩
Proof state after:
no goals