chore(MathlibTest): fix defLemma warnings (leanprover-community#40593)

In all these cases, a dummy definition was declared of type True: the `defProp` linter complains that a declaration of type `True` should be a `lemma`. Instead, change to a definition with value (the natural 0).

Author: grunweg

MathlibTest/Linter/DocPrime.lean

@@ -79,7 +79,7 @@ Declarations whose name ends with a `'` are expected to contain an explanation f
 Note: This linter can be disabled with `set_option linter.docPrime false`
 -/
 #guard_msgs in
-abbrev abbrev_no_doc' : True := .intro
+abbrev abbrev_no_doc' : Nat := 0
 
 /--
 warning: `def_no_doc'` is missing a doc-string, please add one.
@@ -88,8 +88,7 @@ Declarations whose name ends with a `'` are expected to contain an explanation f
 Note: This linter can be disabled with `set_option linter.docPrime false`
 -/
 #guard_msgs in
-set_option linter.defProp false in
-def def_no_doc' : True := .intro
+def def_no_doc' := 0
 
 -- Anonymous declarations in a primed namespace should not get flagged by the linter.
 namespace Foo'

MathlibTest/Tactic/Says/Basic.lean

@@ -97,12 +97,11 @@ example : True := by
 -- Check that verification works even with multi-line suggestions, as produced by aesop
 def P : Prop := True
 def Q : Prop := True
-set_option linter.defProp false in
 @[simp]
-def very_long_lemma_name_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : Q → P := fun _ => trivial
-set_option linter.defProp false in
+theorem very_long_lemma_name_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : Q → P := fun _ => trivial
+
 @[simp]
-def very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb : Q := trivial
+theorem very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb : Q := trivial
 /--
 info: Try this:
   [apply] aesop? says