Documentation

Mathlib.Tactic.Contrapose

Contrapose #

The contrapose tactic transforms the goal into its contrapositive when that goal is an implication.

theorem Mathlib.Tactic.Contrapose.mtr {p : Prop} {q : Prop} :
(¬q¬p) → pq

Transforms the goal into its contrapositive.

  • contrapose turns a goal P → Q into ¬ Q → ¬ P
  • contrapose h first reverts the local assumption h, and then uses contrapose and intro h
  • contrapose h with new_h uses the name new_h for the introduced hypothesis
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Transforms the goal into its contrapositive and uses pushes negations inside P and Q. Usage matches contrapose

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For