Mathlib.Tactic.Contrapose

Module docstring

{"# 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

Mathlib.Tactic.Contrapose.mtr theorem

{p q : Prop} : (¬q → ¬p) → (p → q)

Full source

lemma mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) := fun h hp ↦ by_contra (fun h' ↦ h h' hp)

Contrapositive Implication

Informal description

For any propositions $p$ and $q$, the implication $(\neg q \to \neg p)$ implies $(p \to q)$.

Mathlib.Tactic.Contrapose.contrapose definition

: Lean.ParserDescr✝

Full source

/--
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
-/
syntax (name := contrapose) "contrapose" (ppSpace colGt ident (" with " ident)?)? : tactic

Contrapositive tactic

Informal description

The tactic `contrapose` transforms a goal of the form $P \to Q$ into its contrapositive $\neg Q \to \neg P$. Variants include: - `contrapose h` which first reverts the local assumption `h`, then applies `contrapose` and reintroduces `h`. - `contrapose h with new_h` which allows specifying a new name `new_h` for the introduced hypothesis.

Mathlib.Tactic.Contrapose.contrapose! definition

: Lean.ParserDescr✝

Full source

/--
Transforms the goal into its contrapositive and uses pushes negations inside `P` and `Q`.
Usage matches `contrapose`
-/
syntax (name := contrapose!) "contrapose!" (ppSpace colGt ident (" with " ident)?)? : tactic

Contrapositive tactic with negation pushing

Informal description

The tactic `contrapose!` transforms a goal of the form $ P \to Q $ into its contrapositive $ \neg Q \to \neg P $, while also pushing negations inside $ P $ and $ Q $ using the `push_neg` tactic. It can be applied to a goal or to a specific hypothesis, optionally renaming the introduced hypothesis.