If the target of the main goal is a proposition
by_contra' reduces the goal to proving
False using the additional hypothesis
this : ¬ p.
by_contra' h can be used to name the hypothesis
h : ¬ p.
¬ p will be negation normalized using
¬ a < b will be changed to
b ≤ a.
by_contra' h : q will normalize negations in
¬ p, normalize negations in
and then check that the two normalized forms are equal.
The resulting hypothesis is the pre-normalized form,
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
example : 1 < 2 := by by_contra' h -- h : 2 ≤ 1 ⊢ False example : 1 < 2 := by by_contra' h : ¬ 1 < 2 -- h : ¬ 1 < 2 ⊢ False