Theorem: problem_2 (BrownCs22/Homework/Hw1Sols.lean)

State before:
p q r s : Prop
⊢ (p → ¬q) → ¬(p ∧ q)
Tactic:
intro hpnq
State after:
p q r s : Prop
hpnq : p → ¬q
⊢ ¬(p ∧ q)

State before:
p q r s : Prop
hpnq : p → ¬q
⊢ ¬(p ∧ q)
Tactic:
intro hpq
State after:
p q r s : Prop
hpnq : p → ¬q
hpq : p ∧ q
⊢ False

State before:
p q r s : Prop
hpnq : p → ¬q
hpq : p ∧ q
⊢ False
Tactic:
eliminate hpq with hp hq
State after:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
⊢ False

State before:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
⊢ False
Tactic:
have hnq : ¬ q := hpnq hp
State after:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
hnq : ¬q
⊢ False

State before:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
hnq : ¬q
⊢ False
Tactic:
contradiction
State after:
no goals