Theorem: PrependClause.revrelAux (Saturn/PrependClause.lean)

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

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

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

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

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

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

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

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

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

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

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

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)
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 }
Tactic:
rw [lem'] at lem''
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)
      { 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 }
⊢ 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 }

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)
lem'' :
  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 }
⊢ 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:
exact lem''
State after:
no goals

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 (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses
Tactic:
rw [lem]
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 v { val := l, isLt := w } + 1 < succ num_clauses

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 v { val := l, isLt := w } + 1 < succ num_clauses
Tactic:
apply Nat.succ_lt_succ
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
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 v { val := l, isLt := w } < num_clauses

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
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 v { val := l, isLt := w } < num_clauses
Tactic:
exact bd
State after:
no goals

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
⊢ 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) }
Tactic:
apply Fin.eq_of_veq
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
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ ↑(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) }

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
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ ↑(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) }
Tactic:
simp
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
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 v { val := l, isLt := w } + 1 =
    Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) }

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
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 v { val := l, isLt := w } + 1 =
    Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) }
Tactic:
symm
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
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 (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) } =
    Vector.get v { val := l, isLt := w } + 1

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
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 (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) } =
    Vector.get v { val := l, isLt := w } + 1
Tactic:
exact lem
State after:
no goals