internlm/Lean-Github huggingface dataset:
Theorem: concat_empty_seq_id
Proof state before:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ (seq++|FinSeq.empty) k = seq k
Tactic:
apply funext
Proof state after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n + zero), (seq++|FinSeq.empty) k x = seq k x
Theorem: concat_empty_seq_id
Proof state before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n + zero), (seq++|FinSeq.empty) k x = seq k x
Tactic:
intro kw
Proof state after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n + zero
⊢ (seq++|FinSeq.empty) k kw = seq k kw
Theorem: concat_empty_seq_id
Proof state before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n + zero
⊢ (seq++|FinSeq.empty) k kw = seq k kw
Tactic:
apply (concat_aux_eqs rfl seq FinSeq.empty k).left
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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]
Proof 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
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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]
Proof 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
Theorem: insert_delete_id
Proof 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]
Proof 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
Theorem: insert_delete_id
Proof 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]
Proof 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
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof 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
Theorem: insert_delete_id
Proof 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]
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof state after:
no goals
Theorem: insert_delete_id
Proof 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
Proof state after:
no goals
Theorem: elem_not_beyond_vacuously
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
⊢ n ≤ m → elemNotBeyond seq elem m
Tactic:
intro hyp k kw ineq
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ¬seq k kw = elem
Theorem: elem_not_beyond_vacuously
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ¬seq k kw = elem
Tactic:
let inq := Nat.le_trans hyp ineq
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
⊢ ¬seq k kw = elem
Theorem: elem_not_beyond_vacuously
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
⊢ ¬seq k kw = elem
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ¬seq k kw = elem
Theorem: elem_not_beyond_vacuously
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ¬seq k kw = elem
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
Proof state after:
no goals
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
⊢ ¬x = some !b
Tactic:
match b, eqn  with
| true, Or.inr pf =>
   intro hyp
   simp [pf] at hyp
| false, Or.inr pf =>
   intro hyp
   simp [pf] at hyp
| _ , Or.inl pf =>
   intro hyp
   let w := Eq.trans (Eq.symm pf) hyp
   exact Option.noConfusion w
Proof state after:
no goals
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
⊢ ¬x = some !true
Tactic:
intro hyp
Proof state after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
hyp : x = some !true
⊢ False
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some true
hyp : x = some !true
⊢ False
Tactic:
simp [pf] at hyp
Proof state after:
no goals
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
⊢ ¬x = some !false
Tactic:
intro hyp
Proof state after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
hyp : x = some !false
⊢ False
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
pf : x = some false
hyp : x = some !false
⊢ False
Tactic:
simp [pf] at hyp
Proof state after:
no goals
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
⊢ ¬x = some !x✝
Tactic:
intro hyp
Proof state after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
⊢ False
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
⊢ False
Tactic:
let w := Eq.trans (Eq.symm pf) hyp
Proof state after:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
w : none = some !x✝ := pf.symm.trans hyp
⊢ False
Theorem: notpure_cases
Proof state before:
b : Bool
x : Option Bool
eqn : x = none ∨ x = some b
x✝ : Bool
pf : x = none
hyp : x = some !x✝
w : none = some !x✝ := pf.symm.trans hyp
⊢ False
Tactic:
exact Option.noConfusion w
Proof state after:
no goals
Theorem: PosResClause.reverseResolve
Proof state before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
⊢ ∀ (rc : ReductionClauses branch focus focusLt clauses) (head : Clause (n + 1))
    (pos : Vector.get' head focus focusLt = some branch) (l : ℕ) (w : l < rc.num_reducedClauses),
    ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head pos) l w =
      ReductionClauses.reverse rc l w + 1
Tactic:
intro rc head neg l w
Proof state after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Theorem: PosResClause.reverseResolve
Proof state before:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1
Tactic:
let rcN := addPositiveClause  branch focus focusLt clauses rc head neg
Proof state after:
num_clauses n : ℕ
branch : Bool
focus : ℕ
focusLt : focus < n + 1
clauses : Vector (Clause (n + 1)) num_clauses
rc : ReductionClauses branch focus focusLt clauses
head : Clause (n + 1)
neg : Vector.get' head focus focusLt = some branch
l : ℕ
w : l < rc.num_reducedClauses
rcN : ReductionClauses branch focus focusLt (head ::ᵥ clauses) :=
  addPositiveClause branch focus focusLt clauses rc head neg
⊢ ReductionClauses.reverse (addPositiveClause branch focus focusLt clauses rc head neg) l w =
    ReductionClauses.reverse rc l w + 1