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

contrapose transforms the main goal into its contrapositive. If the goal has the form ⊢ P → Q, then contrapose turns it into ⊢ ¬ Q → ¬ P. If the goal has the form ⊢ P ↔ Q, then contraposeturns it into⊢ ¬ P ↔ ¬ Q`.

• contrapose h on a goal of the form h : P ⊢ Q turns the goal into h : ¬ Q ⊢ ¬ P. This is equivalent to revert h; contrapose; intro h.
• contrapose h with new_h uses the name new_h for the introduced hypothesis. This is equivalent to revert h; contrapose; intro new_h.
• contrapose!, contrapose! h and contrapose! h with new_h push negation deeper into the goal after contraposing (but before introducing the new hypothesis). See the push_neg tactic for more details on the pushing algorithm.
• contrapose! (config := cfg) controls the options for negation pushing. All options for Mathlib.Tactic.Push.Config are supported:
  • contrapose! +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q instead of p → ¬ q.

Examples:

variables (P Q R : Prop)

example (H : ¬ Q → ¬ P) : P → Q := by
  contrapose
  exact H

example (H : ¬ P ↔ ¬ Q) : P ↔ Q := by
  contrapose
  exact H

example (H : ¬ Q → ¬ P) (h : P) : Q := by
  contrapose h
  exact H h

example (H : ¬ R → P → ¬ Q) : (P ∧ Q) → R := by
  contrapose!
  exact H

example (H : ¬ R → ¬ P ∨ ¬ Q) : (P ∧ Q) → R := by
  contrapose! +distrib
  exact H

Equations

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

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

contrapose transforms the main goal into its contrapositive. If the goal has the form ⊢ P → Q, then contrapose turns it into ⊢ ¬ Q → ¬ P. If the goal has the form ⊢ P ↔ Q, then contraposeturns it into⊢ ¬ P ↔ ¬ Q`.

• contrapose h on a goal of the form h : P ⊢ Q turns the goal into h : ¬ Q ⊢ ¬ P. This is equivalent to revert h; contrapose; intro h.
• contrapose h with new_h uses the name new_h for the introduced hypothesis. This is equivalent to revert h; contrapose; intro new_h.
• contrapose!, contrapose! h and contrapose! h with new_h push negation deeper into the goal after contraposing (but before introducing the new hypothesis). See the push_neg tactic for more details on the pushing algorithm.
• contrapose! (config := cfg) controls the options for negation pushing. All options for Mathlib.Tactic.Push.Config are supported:
  • contrapose! +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q instead of p → ¬ q.

Examples:

variables (P Q R : Prop)

example (H : ¬ Q → ¬ P) : P → Q := by
  contrapose
  exact H

example (H : ¬ P ↔ ¬ Q) : P ↔ Q := by
  contrapose
  exact H

example (H : ¬ Q → ¬ P) (h : P) : Q := by
  contrapose h
  exact H h

example (H : ¬ R → P → ¬ Q) : (P ∧ Q) → R := by
  contrapose!
  exact H

example (H : ¬ R → ¬ P ∨ ¬ Q) : (P ∧ Q) → R := by
  contrapose! +distrib
  exact H

Equations

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