internlm/Lean-Github huggingface dataset:
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ n < n + 1
Tactic:
omega
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
ih : Interpretation V_N V_T R (R A, xs) (n, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
Tactic:
exact ih ih_1
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ ys.IsPrefix xs
Tactic:
specialize ih n2 _ e2
Proof state after:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ n2 < n1 + n2 + 1

V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
ih : Interpretation V_N V_T R (e2, xs) (n2, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ n2 < n1 + n2 + 1
Tactic:
omega
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
ih : Interpretation V_N V_T R (e2, xs) (n2, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
Tactic:
exact ih ih_2
Proof state after:
no goals
Theorem: invertible_id
Proof state before:
α : Sort u_1
⊢ invertible id
Tactic:
have : isInv (id : α → α) id := by
  apply And.intro
  . intro x
    simp
  . intro y
    simp
Proof state after:
α : Sort u_1
this : isInv id id
⊢ invertible id
Theorem: invertible_id
Proof state before:
α : Sort u_1
this : isInv id id
⊢ invertible id
Tactic:
exact ⟨id, this⟩
Proof state after:
no goals
Theorem: invertible_id
Proof state before:
α : Sort u_1
⊢ isInv id id
Tactic:
apply And.intro
Proof state after:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x

case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Theorem: invertible_id
Proof state before:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x

case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
. intro x
  simp
Proof state after:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Theorem: invertible_id
Proof state before:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
. intro y
  simp
Proof state after:
no goals
Theorem: invertible_id
Proof state before:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x
Tactic:
intro x
Proof state after:
case left
α : Sort u_1
x : α
⊢ id (id x) = x
Theorem: invertible_id
Proof state before:
case left
α : Sort u_1
x : α
⊢ id (id x) = x
Tactic:
simp
Proof state after:
no goals
Theorem: invertible_id
Proof state before:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
intro y
Proof state after:
case right
α : Sort u_1
y : α
⊢ id (id y) = y
Theorem: invertible_id
Proof state before:
case right
α : Sort u_1
y : α
⊢ id (id y) = y
Tactic:
simp
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof 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⟩⟩
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof 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]
Proof state after:
no goals
Theorem: permuted_map_invertible
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 : invertible p.to_map
⊢ invertible (permuted.step i j fi ij jl p).to_map
Tactic:
let ⟨f', ⟨h1, h2⟩⟩ := 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 : 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
Theorem: permuted_map_invertible
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 : 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)
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 : 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
Theorem: permuted_map_invertible
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 : 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
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 : 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
Theorem: permuted_map_invertible
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 : 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'
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 : 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
Theorem: permuted_map_invertible
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 : 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]
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 : 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
Theorem: permuted_map_invertible
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 : 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]
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 : 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
Theorem: permuted_map_invertible
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 : 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⟩⟩
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'
⊢ ∀ (x : Fin n), g (f x) = x
Tactic:
intro x
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 : 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
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'
x : Fin n
⊢ g (f x) = x
Tactic:
simp (config := {zeta := false}) [f, permuted.to_map]
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 : 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
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'
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]
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof 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]
Proof state after:
no goals
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'
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]
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'
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]
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'
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]
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), f (g y) = y
Tactic:
intro y
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 : 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
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
⊢ f (g y) = y
Tactic:
simp (config := {zeta := false}) [g]
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 : 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
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
⊢ 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
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 : 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
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
⊢ 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]
Proof state after:
no goals
Theorem: permuted_map_invertible
Proof 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]
Proof state after:
no goals