Theorem: HW2.bonus_challenge (BrownCs22/Homework/Hw2sols.lean)

State before:
p : Prop
⊢ ¬(p ↔ ¬p)
Tactic:
intro hiff
State after:
p : Prop
hiff : p ↔ ¬p
⊢ False

State before:
p : Prop
hiff : p ↔ ¬p
⊢ False
Tactic:
eliminate hiff with h_left h_right
State after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ False

State before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ False
Tactic:
have hnp : ¬ p
State after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p

case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False

State before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p

case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Tactic:
{ intro hp 
  have hnp : ¬ p := h_left hp
  contradiction }
State after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False

State before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Tactic:
have hp : p := h_right hnp
State after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
hp : p
⊢ False

State before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
hp : p
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p
Tactic:
intro hp
State after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
⊢ False

State before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
⊢ False
Tactic:
have hnp : ¬ p := h_left hp
State after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
hnp : ¬p
⊢ False

State before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
hnp : ¬p
⊢ False
Tactic:
contradiction
State after:
no goals