structure projections and def_lemma linter

Stream: general

[Junyan Xu]

currently blocking #18013

import tactic.lint.default

/-- -/
structure A : Prop := (x : true)

#print A.x
/- This should ideally be `lemma` rather than `@[reducible] def`:
@[reducible]
def A.x : A → true :=
λ (self : A), [A.x self]
-/

alias A.x ← x
/- `A.x` itself doesn't trigger the def_lemma linter, but creating an alias triggers it. -/

#lint
/-
/- Checking 2 declarations (plus 8 automatically generated ones) in the current file with 26 linters -/

/- The `def_lemma` linter reports: -/
/- INCORRECT DEF/LEMMA: -/
#check @x /- is a def, should be a lemma/theorem -/
-/

[Junyan Xu]

Another (possibly unrelated) problem is that the universe of a structure seems to default to Type (not Type*, not Sort*) even if all its fields are Props.

structure A := (x : true)
#print A
/-
structure A : Type
fields:
A.x : A → true
-/

This has caused some unintended universes in mathlib, like docs#category_theory.monoidal_preadditive and docs#category_theory.monoidal_linear. But it's easy to fix, just add : Prop.