by_contra' #

by_contra' is a tactic for proving propositions by contradiction. It is similar to by_contra except that it also uses push_neg to normalize negations.

source

meta def tactic.interactive.by_contra' (h : interactive.parse (optional lean.parser.ident)) (t : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) :

tactic unit

If the target of the main goal is a proposition p, by_contra' reduces the goal to proving false using the additional hypothesis h : ¬ p. by_contra' h can be used to name the hypothesis h : ¬ p. The hypothesis ¬ p will be negation normalized using push_neg. For instance, ¬ a < b will be changed to b ≤ a. by_contra' h : q will normalize negations in ¬ 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 (tactic.interactive.by_contra).

Examples:

example : 1 < 2 :=
begin
  by_contra' h,
  -- h : 2 ≤ 1 ⊢ false
end

example : 1 < 2 :=
begin
  by_contra' h : ¬ 1 < 2,
  -- h : ¬ 1 < 2 ⊢ false
end
```

source

def tactic_doc.tactic.by_contra' :

tactic_doc_entry

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 (tactic.interactive.by_contra).

Examples:

example : 1 < 2 :=
begin
  by_contra' h,
  -- h : 2 ≤ 1 ⊢ false
end

example : 1 < 2 :=
begin
  by_contra' h : ¬ 1 < 2,
  -- h : ¬ 1 < 2 ⊢ false
end
```