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

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

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

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

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

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