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

State before:
P : Prop
⊢ ¬P → P → False
Tactic:
intros
State after:
P : Prop
a✝¹ : ¬P
a✝ : P
⊢ False

State before:
P : Prop
a✝¹ : ¬P
a✝ : P
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
P : Prop
⊢ (P → False) → ¬P
Tactic:
intro f
State after:
P : Prop
f : P → False
⊢ ¬P

State before:
P : Prop
f : P → False
⊢ ¬P
Tactic:
exact f
State after:
no goals