mathlib-review

# Mathlib PR Review ## Attributes and API - New definitions should come with associated lemmas and appropriate attributes (`@[simp]`, `@[ext]`, etc.). - Watch for instance diamonds. - Prefer bundled morphisms, `FunLike` API for morphism classes, `SetLike` API for subobject classes. ## Style Points Specific to Mathlib - **Simp squeezing:** Terminal `simp` calls should NOT be squeezed (replaced with `simp only [...]`) unless there's a measured performance problem. Unsqueezed `simp` is more maintainable and doesn't break when lemmas are renamed. - **Normal forms:** Prefer `s.Nonempty` over alternatives. Use `hne : x ≠ ⊥` in hypotheses (easier to check), `hlt : ⊥ < x` in conclusions (more powerful). - **Transparency:** Needing `erw`, or `rfl` after `simp`/`rw` usually means the API is missing lemmas. - **File size:** Consider splitting files that exceed ~1000 lines or cover multiple topics. ## Reference Guides The full review guide and style references: - **Review guide:** https://leanprover-community.github.io/contribute/pr-review.html - **Naming conventions:** https://leanprover-community.github.io/contribute/naming.html - **Code style:** https://leanprover-community.github.io/contribute/style.html - **Documentation style:** https://leanprover-community.github.io/contribute/doc.html