Theorem: permuted_map_invertible (QuickSortInLean/Permutation.lean)

State before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
⊢ invertible p.to_map
Tactic:
induction p with
| refl => simp [permuted.to_map, invertible_id]
| step i j fi ij jl p ih =>
  let ⟨f', ⟨h1, h2⟩⟩ := ih
  let f := permuted.to_map (permuted.step i j fi ij jl p)
  show invertible f
  let g := fun (k : Fin n) =>
    let k' := f' k
    if k' = i then j
    else if k' = j then i
    else k'
  have gf : ∀x, g (f x) = x := by
    intro x
    simp (config := {zeta := false}) [f, permuted.to_map]
    cases decEq x i with
    | isFalse nxi =>
      cases decEq x j with
      | isFalse nxj => simp [nxi, nxj, g, h1]
      | isTrue xj => simp [nxi, xj, g, h1]
    | isTrue xi => simp [xi, g, h1]
  have fg : ∀y, f (g y) = y := by
    intro y
    simp (config := {zeta := false}) [g]
    show f (if f' y = i then j else if f' y = j then i else f' y) = y
    cases decEq (f' y) i with
    | isFalse nfyi =>
      cases decEq (f' y) j with
      | isFalse nfyj => simp [nfyi, nfyj, permuted.to_map, h2, f]
      | isTrue fyj =>
        simp [nfyi, fyj, permuted.to_map, f]
        rw [←(congrArg p.to_map fyj), h2]
    | isTrue fyi =>
      simp [fyi, f, permuted.to_map]
      have : (if j = i then j else i) = i := by simp
      rw [this, ←(congrArg p.to_map fyi), h2]
  exact ⟨g, ⟨gf, fg⟩⟩
State after:
no goals

State before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ : Vec α✝ n
⊢ invertible permuted.refl.to_map
Tactic:
simp [permuted.to_map, invertible_id]
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 : invertible p.to_map
⊢ invertible (permuted.step i j fi ij jl p).to_map
Tactic:
let ⟨f', ⟨h1, h2⟩⟩ := 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 : 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
⊢ invertible (permuted.step i j fi ij jl p).to_map

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 : 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
⊢ invertible (permuted.step i j fi ij jl p).to_map
Tactic:
let f := permuted.to_map (permuted.step i j fi ij jl p)
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 : 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
⊢ invertible (permuted.step i j fi ij jl p).to_map

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 : 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
⊢ invertible (permuted.step i j fi ij jl p).to_map
Tactic:
show invertible f
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 : 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
⊢ invertible f

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 : 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
⊢ invertible f
Tactic:
let g := fun (k : Fin n) =>
  let k' := f' 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 : 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'
⊢ invertible f

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 : 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'
⊢ invertible f
Tactic:
have gf : ∀x, g (f x) = x := by
  intro x
  simp (config := {zeta := false}) [f, permuted.to_map]
  cases decEq x i with
  | isFalse nxi =>
    cases decEq x j with
    | isFalse nxj => simp [nxi, nxj, g, h1]
    | isTrue xj => simp [nxi, xj, g, h1]
  | isTrue xi => simp [xi, g, h1]
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 : 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
⊢ invertible f

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 : 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
⊢ invertible f
Tactic:
have fg : ∀y, f (g y) = y := by
  intro y
  simp (config := {zeta := false}) [g]
  show f (if f' y = i then j else if f' y = j then i else f' y) = y
  cases decEq (f' y) i with
  | isFalse nfyi =>
    cases decEq (f' y) j with
    | isFalse nfyj => simp [nfyi, nfyj, permuted.to_map, h2, f]
    | isTrue fyj =>
      simp [nfyi, fyj, permuted.to_map, f]
      rw [←(congrArg p.to_map fyj), h2]
  | isTrue fyi =>
    simp [fyi, f, permuted.to_map]
    have : (if j = i then j else i) = i := by simp
    rw [this, ←(congrArg p.to_map fyi), h2]
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 : 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
fg : ∀ (y : Fin n), f (g y) = y
⊢ invertible f

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 : 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
fg : ∀ (y : Fin n), f (g y) = y
⊢ invertible f
Tactic:
exact ⟨g, ⟨gf, fg⟩⟩
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 : 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'
⊢ ∀ (x : Fin n), g (f x) = x
Tactic:
intro x
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 : 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'
x : Fin n
⊢ g (f x) = x

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'
x : Fin n
⊢ g (f x) = x
Tactic:
simp (config := {zeta := false}) [f, permuted.to_map]
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 : 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'
x : Fin n
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x

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'
x : Fin n
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x
Tactic:
cases decEq x i with
| isFalse nxi =>
  cases decEq x j with
  | isFalse nxj => simp [nxi, nxj, g, h1]
  | isTrue xj => simp [nxi, xj, g, h1]
| isTrue xi => simp [xi, g, h1]
State after:
no goals

State before:
case 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'
x : Fin n
nxi : ¬x = i
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x
Tactic:
cases decEq x j with
| isFalse nxj => simp [nxi, nxj, g, h1]
| isTrue xj => simp [nxi, xj, g, h1]
State after:
no goals

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'
x : Fin n
nxi : ¬x = i
nxj : ¬x = j
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x
Tactic:
simp [nxi, nxj, g, h1]
State after:
no goals

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'
x : Fin n
nxi : ¬x = i
xj : x = j
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x
Tactic:
simp [nxi, xj, g, h1]
State after:
no goals

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'
x : Fin n
xi : x = i
⊢ g
      (let k' := if x = i then j else if x = j then i else x;
      p.to_map k') =
    x
Tactic:
simp [xi, g, h1]
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 : 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), f (g y) = y
Tactic:
intro y
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 : 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
⊢ f (g y) = y

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
⊢ f (g y) = y
Tactic:
simp (config := {zeta := false}) [g]
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 : 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
⊢ f
      (let k' := f' y;
      if k' = i then j else if k' = j then i else k') =
    y

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
⊢ f
      (let k' := f' y;
      if k' = i then j else if k' = j then i else k') =
    y
Tactic:
show f (if f' y = i then j else if f' y = j then i else f' y) = y
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 : 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
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y

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
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
Tactic:
cases decEq (f' y) i with
| isFalse nfyi =>
  cases decEq (f' y) j with
  | isFalse nfyj => simp [nfyi, nfyj, permuted.to_map, h2, f]
  | isTrue fyj =>
    simp [nfyi, fyj, permuted.to_map, f]
    rw [←(congrArg p.to_map fyj), h2]
| isTrue fyi =>
  simp [fyi, f, permuted.to_map]
  have : (if j = i then j else i) = i := by simp
  rw [this, ←(congrArg p.to_map fyi), h2]
State after:
no goals

State before:
case 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
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
Tactic:
cases decEq (f' y) j with
| isFalse nfyj => simp [nfyi, nfyj, permuted.to_map, h2, f]
| isTrue fyj =>
  simp [nfyi, fyj, permuted.to_map, f]
  rw [←(congrArg p.to_map fyj), h2]
State after:
no goals

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]
State after:
no goals

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]
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

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]
State after:
no goals

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]
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

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
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

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]
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 : 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
State after:
no goals