Theorem: unitClause_skipping_literal (Saturn/Clause.lean)

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ ∀ (i : ℕ) (iw : i < n), get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
intro i iw
State after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
rw [unitClause, Vector.of_Fn'_get']
State after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
let ins := insert_at_image (some b) n k w ((contradiction n).get') i iw
State after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
ins : FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) =
  get' (contradiction n) i iw :=
  insert_at_image (some b) n k w (get' (contradiction n)) i iw
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
ins : FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) =
  get' (contradiction n) i iw :=
  insert_at_image (some b) n k w (get' (contradiction n)) i iw
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
rw [ins, get'_contradiction]
State after:
no goals