Contrapose

The contrapose tactic transforms the goal into its contrapositive when that goal is an implication or an iff. It also avoids creating a double negation if there already is a negation.

• contrapose turns a goal P → Q into ¬ Q → ¬ P and a goal P ↔ Q into ¬ P ↔ ¬ Q
• contrapose! runs contrapose and then 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

opaque Mathlib.Tactic.Contrapose.contrapose.negate_iff : Lean.Option Bool

An option to turn off the feature that contrapose negates both sides of ↔ goals. This may be useful for teaching.

theorem Mathlib.Tactic.Contrapose.contrapose₁ {p q : Prop} : (¬q → ¬p) → p → q

theorem Mathlib.Tactic.Contrapose.contrapose₂ {p q : Prop} : (¬q → p) → ¬p → q

theorem Mathlib.Tactic.Contrapose.contrapose₃ {p q : Prop} : (q → ¬p) → p → ¬q

theorem Mathlib.Tactic.Contrapose.contrapose₄ {p q : Prop} : (q → p) → ¬p → ¬q

theorem Mathlib.Tactic.Contrapose.contrapose_iff₁ {p q : Prop} : (¬p ↔ ¬q) → (p ↔ q)

theorem Mathlib.Tactic.Contrapose.contrapose_iff₂ {p q : Prop} : (p ↔ ¬q) → (¬p ↔ q)

theorem Mathlib.Tactic.Contrapose.contrapose_iff₃ {p q : Prop} : (¬p ↔ q) → (p ↔ ¬q)

theorem Mathlib.Tactic.Contrapose.contrapose_iff₄ {p q : Prop} : (p ↔ q) → (¬p ↔ ¬q)

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

Transforms the goal into its contrapositive.

• contrapose turns a goal P → Q into ¬ Q → ¬ P and it turns a goal P ↔ Q into ¬ P ↔ ¬ Q
• 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 pushes negations in the result. Usage matches contrapose

Equations

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