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

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

State before:
P Q : Prop
h : ¬(P → Q)
⊢ ¬Q
Tactic:
cases Classical.em Q with
| inl q  => exact False.elim (h (λ _ => q))
| inr nq => exact nq
State after:
no goals

State before:
case inl
P Q : Prop
h : ¬(P → Q)
q : Q
⊢ ¬Q
Tactic:
exact False.elim (h (λ _ => q))
State after:
no goals

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