contrapose! — Mathlib

Lean4
/-- Transforms the goal into its contrapositive and uses pushes negations inside `P` and `Q`.
Usage matches `contrapose`
-/
@[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))))))
Похожие утверждения