Theorem: resolution (Test/Bool/Resolution.lean)

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

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

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