nontriviality — Mathlib

Lean4
/-- The `@[nontriviality]` simp set is used by the `nontriviality` tactic to automatically
discharge theorems about the trivial case (where we know `Subsingleton α` and many theorems
in e.g. groups are trivially true). -/
@[attr_parser 1000]
public meta def nontriviality : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Parser.Attr.nontriviality 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "nontriviality" false✝)
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost)))
        (ParserDescr.unary✝ `optional
          (ParserDescr.unary✝ `patternIgnore
            (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "← " `token.«← » (ParserDescr.symbol✝ "← "))
              (ParserDescr.nodeWithAntiquot✝ "<- " `token.«<- » (ParserDescr.symbol✝ "<- "))))))
      (ParserDescr.unary✝ `optional (ParserDescr.cat✝ `prio 0)))
Похожие утверждения