Name: Mathlib Review
Author: leanprover

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.

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 , or after / usually means the API is missing lemmas.

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.

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 , or after / usually means the API is missing lemmas.