Theorem: isPure_of_PureTail_at_zero (Saturn/Clause.lean)

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
⊢ HasPureTail clauses index bound parity zero → IsPure clauses index bound parity
Tactic:
intro hyp
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
⊢ IsPure clauses index bound parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
⊢ IsPure clauses index bound parity
Tactic:
intro k
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Tactic:
intro kw
State after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
kw : k < num_clauses
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity

State before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
kw : k < num_clauses
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
exact hyp k kw  (Nat.zero_le k)
State after:
no goals