Theorem: insert_delete_id (Saturn/FinSeq.lean)

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : j = k
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
match j, jw, c with
| .(k), .(kw), rfl => apply insert_at_focus
State after:
no goals

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : j = k
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) k kw = seq k kw
Tactic:
apply insert_at_focus
State after:
no goals

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let i := skipInverse k j c
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let eqn : skip k i = j  := skipInverse_eq k j c
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let iw : i < n := skip_preimage_lt kw jw eqn
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let lem1 : insert (seq k kw) n k kw (delete k kw seq) j jw
  = insert (seq k kw) n k kw (delete k kw seq) (skip k i) (skip_le_succ iw) :=
    by
      apply witness_independent
      rw [← eqn]
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let lem2 : insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) =
              delete k kw seq i iw := by apply insert_at_image
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
let resolve : delete k kw seq i iw = seq (skip k i) (skip_le_succ iw) := by rfl
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw = seq j jw
Tactic:
rw [lem1]
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = seq j jw
Tactic:
rw [lem2]
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ delete k kw seq i iw = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ delete k kw seq i iw = seq j jw
Tactic:
rw [resolve]
State after:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ seq (skip k i) (_ : skip k i < n + 1) = seq j jw

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ seq (skip k i) (_ : skip k i < n + 1) = seq j jw
Tactic:
apply witness_independent
State after:
case a
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ skip k i = j

State before:
case a
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
resolve : delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1) := Eq.refl (delete k kw seq i iw)
⊢ skip k i = j
Tactic:
exact eqn
State after:
no goals

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
    FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1)
Tactic:
apply witness_independent
State after:
case a
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
⊢ j = skip k i

State before:
case a
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
⊢ j = skip k i
Tactic:
rw [← eqn]
State after:
no goals

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
⊢ FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) ?m.13251 = delete k kw seq i iw
Tactic:
apply insert_at_image
State after:
no goals

State before:
α : Type
n k : ℕ
kw : k < n + 1
seq : FinSeq (n + 1) α
j : ℕ
jw : j < succ n
c : ¬j = k
i : ℕ := skipInverse k j c
eqn : skip k i = j := skipInverse_eq k j c
iw : i < n := skip_preimage_lt kw jw eqn
lem1 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) j jw =
  FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) :=
  witness_independent (fun j => FinSeq.insert (seq k kw) n k kw (delete k kw seq) j) j (skip k i) jw (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip k i) eqn.symm)) (Eq.refl (skip k i)))
lem2 : FinSeq.insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = delete k kw seq i iw :=
  insert_at_image (seq k kw) n k kw (delete k kw seq) i iw
⊢ delete k kw seq i iw = seq (skip k i) (_ : skip k i < n + 1)
Tactic:
rfl
State after:
no goals