Theorem: MyNat.contra (TheoremProvingLean/inductive_types.lean)

State before:
P Q : Prop
⊢ P ∧ ¬P → Q
Tactic:
intro h
State after:
P Q : Prop
h : P ∧ ¬P
⊢ Q

State before:
P Q : Prop
h : P ∧ ¬P
⊢ Q
Tactic:
cases h with
| intro hp hnp => contradiction
State after:
no goals

State before:
case intro
P Q : Prop
hp : P
hnp : ¬P
⊢ Q
Tactic:
contradiction
State after:
no goals