feat(library/init/meta/tactic): add dec_trivial notation

library/init/meta/tactic.lean

@@ -654,6 +654,8 @@ infer_type fn >>= get_pi_arity
 
 meta def triv : tactic unit := mk_const `trivial >>= exact
 
+notation `dec_trivial` := of_as_true (by tactic.triv)
+
 meta def by_contradiction (H : name) : tactic expr :=
 do tgt : expr ← target,
    (match_not tgt >> return ())

tests/lean/run/find.lean

@@ -1,6 +1,4 @@
 open nat
 
-notation `dec_trivial` := of_as_true (by tactic.triv)
-
 lemma aux : ∃ x : nat, x > 10 :=
 exists.intro 15 dec_trivial

tests/lean/run/size_of1.lean

@@ -1,7 +1,5 @@
 open tactic
 
-notation `dec_trivial` := of_as_true (by triv)
-
 example : sizeof [tt, tt] < sizeof [tt, ff, tt] :=
 dec_trivial