trivial

trivial は明らかな(trivial)ことを示します．

-- True は何の仮定もなしに示せる
example : True := by trivial

-- 定義から明らかな等式
example : 1 + 1 = 2 := by trivial

-- 矛盾があるので, どんな命題でも証明できる
example (P : Prop) (h : False) : P := by trivial

舞台裏

trivial は，複数のタクティクを順に試すマクロとして実装されています．trace.Elab.step というオプションを true にすると，展開の様子を順を追って見ることができます.

/--
info: [Elab.step] trivial
  [Elab.step] trivial
    [Elab.step] trivial
      [Elab.step] (apply And.intro✝) <;> trivial
        [Elab.step] focus
              apply And.intro✝
              with_annotate_state"<;>" skip
              all_goals trivial
          [Elab.step] ⏎
                apply And.intro✝
                with_annotate_state"<;>" skip
                all_goals trivial
            [Elab.step] ⏎
                  apply And.intro✝
                  with_annotate_state"<;>" skip
                  all_goals trivial
              [Elab.step] apply And.intro✝
      [Elab.step] apply True.intro✝
      [Elab.step] decide
      [Elab.step] contradiction
-/
#guard_msgs in
example (P : Prop) (h : False) : P := by
  set_option trace.Elab.step true in
  trivial

出力が長いのですが，まず apply And.intro を試し，次に apply True.intro を試し，次に decide と contradiction を試していることがわかります．