Theorem: Smt.Reconstruct.Prop.notImplies1 (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {P Q : Prop}, ¬(P → Q) → P
Tactic:
intros P Q h
State after:
P Q : Prop
h : ¬(P → Q)
⊢ P

State before:
P Q : Prop
h : ¬(P → Q)
⊢ P
Tactic:
cases Classical.em P with
| inl p  => exact p
| inr np => apply False.elim
            apply h
            intro p
            exact False.elim (np p)
State after:
no goals

State before:
case inl
P Q : Prop
h : ¬(P → Q)
p : P
⊢ P
Tactic:
exact p
State after:
no goals

State before:
case inr
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P
Tactic:
apply False.elim
State after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ False

State before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ False
Tactic:
apply h
State after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P → Q

State before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P → Q
Tactic:
intro p
State after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
p : P
⊢ Q

State before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
p : P
⊢ Q
Tactic:
exact False.elim (np p)
State after:
no goals