Lean4
/-- 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`.
`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`.
Examples:
```lean
example : 1 < 2 := by
by_contra! h
-- h : 2 ≤ 1 ⊢ False
example : 1 < 2 := by
by_contra! h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
```
-/
@[tactic_parser 1000]
public meta def byContra! : Lean.ParserDescr✝ :=
ParserDescr.node✝ `byContra! 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "by_contra!" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt)) Lean.binderIdent)))
(ParserDescr.parser✝ `Lean.Parser.Term.optType))
