internlm/Lean-Github huggingface dataset:
Theorem: PrependClause.forwardResolve
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) { val := l + 1, isLt := w } =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })
Tactic:
have s : { val := l + 1, isLt := w } = Fin.succ
  ⟨l, le_of_succ_le_succ w⟩ := by rfl
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) { val := l + 1, isLt := w } =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })
Theorem: PrependClause.forwardResolve
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) { val := l + 1, isLt := w } =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })
Tactic:
rw [s]
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec)
      (Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }) =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })
Theorem: PrependClause.forwardResolve
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
⊢ Vector.get (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec)
      (Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }) =
    Option.map (fun x => x + 1) (Vector.get rc.forwardVec { val := l, isLt := (_ : succ l ≤ num_clauses) })
Tactic:
rw [Vector.get_cons_succ, Vector.get_map]
Proof state after:
no goals
Theorem: PrependClause.forwardResolve
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < num_clauses + 1
⊢ { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
Tactic:
rfl
Proof state after:
no goals
Theorem: PrependClause.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 : ¬get' head focus focusLt = some branch) (l : ℕ) (w : l + 1 < rc.num_reducedClauses + 1),
    ReductionClauses.reverse (prependClause branch focus focusLt clauses rc head neg) (l + 1) w =
      ReductionClauses.reverse rc l (_ : succ l ≤ rc.num_reducedClauses) + 1
Tactic:
intro rc head _ 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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
⊢ ReductionClauses.reverse (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    ReductionClauses.reverse rc l (_ : succ l ≤ rc.num_reducedClauses) + 1
Theorem: PrependClause.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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
⊢ ReductionClauses.reverse (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    ReductionClauses.reverse rc l (_ : succ l ≤ rc.num_reducedClauses) + 1
Tactic:
simp [ReductionClauses.reverse, ReductionClauses.reverseVec, prependClause, Vector.get', get'_map]
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) rc.reverseVec) { val := l + 1, isLt := w } =
    Vector.get rc.reverseVec { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) } + 1
Theorem: PrependClause.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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) rc.reverseVec) { val := l + 1, isLt := w } =
    Vector.get rc.reverseVec { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) } + 1
Tactic:
have s : { val := l + 1, isLt := w } = Fin.succ
        ⟨l, le_of_succ_le_succ w⟩ := by rfl
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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) }
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) rc.reverseVec) { val := l + 1, isLt := w } =
    Vector.get rc.reverseVec { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) } + 1
Theorem: PrependClause.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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
s : { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) }
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) rc.reverseVec) { val := l + 1, isLt := w } =
    Vector.get rc.reverseVec { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) } + 1
Tactic:
rw [s, Vector.get_cons_succ, Vector.get_map]
Proof state after:
no goals
Theorem: PrependClause.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✝ : ¬get' head focus focusLt = some branch
l : ℕ
w : l + 1 < rc.num_reducedClauses + 1
⊢ { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ rc.num_reducedClauses) }
Tactic:
rfl
Proof state after:
no goals
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses
Tactic:
have l : Vector.get (0 ::ᵥ map (fun x ↦ x + 1) v) (Fin.succ { val := l, isLt := w }) =  v.get ⟨l, w⟩ + 1  := by
  rw [Vector.get_cons_succ]
  rw [Vector.get_map]
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) < succ num_clauses
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) < succ num_clauses
Tactic:
rw [l]
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get v { val := l✝, isLt := w } + 1 < succ num_clauses
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get v { val := l✝, isLt := w } + 1 < succ num_clauses
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get v { val := l✝, isLt := w } < num_clauses
Theorem: PrependClause.revrelAux
Proof state before:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l✝ : ℕ
w : l✝ < num_reducedClauses
bd : Vector.get v { val := l✝, isLt := w } < num_clauses
l :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l✝, isLt := w }) =
    Vector.get v { val := l✝, isLt := w } + 1
⊢ Vector.get v { val := l✝, isLt := w } < num_clauses
Tactic:
exact bd
Proof state after:
no goals
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
Tactic:
rw [Vector.get_cons_succ]
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (map (fun x => x + 1) v) { val := l, isLt := w } = Vector.get v { val := l, isLt := w } + 1
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (map (fun x => x + 1) v) { val := l, isLt := w } = Vector.get v { val := l, isLt := w } + 1
Tactic:
rw [Vector.get_map]
Proof state after:
no goals
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
    Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) }
Tactic:
symm
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
let lem :=
  Vector.get_cons_succ 0 (map (fun x ↦ x + 1) v) ⟨l, w⟩
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
  Vector.get (map (fun x => x + 1) v) { val := l, isLt := w } :=
  get_cons_succ 0 (map (fun x => x + 1) v) { val := l, isLt := w }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
  Vector.get (map (fun x => x + 1) v) { val := l, isLt := w } :=
  get_cons_succ 0 (map (fun x => x + 1) v) { val := l, isLt := w }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
rw [Vector.get_map] at lem
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
let lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  ⟨ Vector.get (0 ::ᵥ map (fun x ↦ x + 1) v) (Fin.succ { val := l, isLt := w }), by
      rw [lem]
      apply Nat.succ_lt_succ
      exact bd
  ⟩  := by
    apply Fin.eq_of_veq
    simp
    symm
    exact lem
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
let lem'' :=
  Vector.get_cons_succ head clauses ⟨Vector.get v { val := l, isLt := w }, bd⟩
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
lem'' : Vector.get (head ::ᵥ clauses) (Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd }) =
  Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd } :=
  get_cons_succ head clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }