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

State before:
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P
Tactic:
repeat (rw [not_iff_imp_false])
State after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False

State before:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False
Tactic:
exact imp_trans P Q False
State after:
no goals

State before:
P Q : Prop
⊢ (P → Q) → (Q → False) → ¬P
Tactic:
(rw [not_iff_imp_false])
State after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False

State before:
P Q : Prop
⊢ (P → Q) → (Q → False) → ¬P
Tactic:
rw [not_iff_imp_false]
State after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False