Theorem: disjunctive_syllogism (Test/Bool/DisjunctiveSyllogism.lean)

State before:
p q : Bool
⊢ (p || q) = true → (!p) = true → q = true
Tactic:
intro hpq hnp
State after:
p q : Bool
hpq : (p || q) = true
hnp : (!p) = true
⊢ q = true

State before:
p q : Bool
hpq : (p || q) = true
hnp : (!p) = true
⊢ q = true
Tactic:
cases p <;> simp_all
State after:
no goals