contrapose — Mathlib

Lean4
/-- Transforms the goal into its contrapositive.
* `contrapose`     turns a goal `P → Q` into `¬ Q → ¬ P`
* `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
-/
@[tactic_parser 1000]
public meta def contrapose : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Contrapose.contrapose 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "contrapose" false✝)
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
            (ParserDescr.const✝ `ident))
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ") (ParserDescr.const✝ `ident))))))
Похожие утверждения