# Documentation

Mathlib.Tactic.Contrapose

# Contrapose #

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

• contrapose turns a goal P → Q→ Q into ¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ P
• contrapose! turns a goal P → Q→ Q into ¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ P and pushes negations inside P and Q using push_neg
• contrapose h first reverts the local assumption h, and then uses contrapose and intro h
• 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
theorem Mathlib.Tactic.Contrapose.mtr {p : Prop} {q : Prop} :
(¬q¬p) → pq

Transforms the goal into its contrapositive.

• contrapose turns a goal P → Q→ Q into ¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ 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.

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.