Contrapose

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

• contrapose turns a goal P → Q into ¬ Q → ¬ P
• contrapose! turns a goal P → Q into ¬ Q → ¬ 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) → p → q

def Mathlib.Tactic.Contrapose.contrapose : Lean.ParserDescr

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.

def Mathlib.Tactic.Contrapose.contrapose! : Lean.ParserDescr

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.