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

State before:
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Tactic:
by_cases P <;> by_cases Q <;> simp [*]
State after:
no goals