Theorem: PrependClause.forwardResolve (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 < num_clauses + 1),
    ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg) (l + 1) w =
      Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))
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 < num_clauses + 1
⊢ ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))

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
⊢ ReductionClauses.forward (prependClause branch focus focusLt clauses rc head neg✝) (l + 1) w =
    Option.map (fun x => x + 1) (ReductionClauses.forward rc l (_ : succ l ≤ num_clauses))
Tactic:
simp [ReductionClauses.forward, ReductionClauses.forwardVec, prependClause]
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
⊢ get' (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) (l + 1) w =
    Option.map (fun x => x + 1) (get' rc.forwardVec l (_ : succ l ≤ num_clauses))

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
⊢ get' (some 0 ::ᵥ map (fun nop => Option.map (fun x => x + 1) nop) rc.forwardVec) (l + 1) w =
    Option.map (fun x => x + 1) (get' rc.forwardVec l (_ : succ l ≤ num_clauses))
Tactic:
simp [Vector.get']
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
⊢ 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) })

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

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

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]
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 < num_clauses + 1
⊢ { val := l + 1, isLt := w } = Fin.succ { val := l, isLt := (_ : succ l ≤ num_clauses) }
Tactic:
rfl
State after:
no goals