Documentation

Mathlib.Tactic.ByContra

If the target of the main goal is a proposition p, by_contra' reduces the goal to proving False using the additional hypothesis this : ¬ p¬ p. by_contra' h can be used to name the hypothesis h : ¬ p¬ p. The hypothesis ¬ p¬ p will be negation normalized using push_neg. For instance, ¬ a < b¬ a < b will be changed to b ≤ a≤ a. by_contra' h : q will normalize negations in ¬ p¬ p, normalize negations in q, and then check that the two normalized forms are equal. The resulting hypothesis is the pre-normalized form, q. If the name h is not explicitly provided, then this will be used as name. This tactic uses classical reasoning. It is a variant on the tactic by_contra. Examples:

example : 1 < 2 := by
  by_contra' h
  -- h : 2 ≤ 1 ⊢ False

example : 1 < 2 := by
  by_contra' h : ¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False
≤ 1 ⊢ False

example : 1 < 2 := by
  by_contra' h : ¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False
⊢ False

example : 1 < 2 := by
  by_contra' h : ¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2 ⊢ False
⊢ False
Equations
  • One or more equations did not get rendered due to their size.