From lean
Provides Mathlib PR review guidelines for Lean: attributes/API, style (simp squeezing, normal forms, transparency), file size tips, and reference links. Use for PR reviews and code quality checks.
npx claudepluginhub leanprover/skills --plugin leanThis skill uses the workspace's default tool permissions.
- New definitions should come with associated lemmas and appropriate attributes (`@[simp]`, `@[ext]`, etc.).
Searches, retrieves, and installs Agent Skills from prompts.chat registry using MCP tools like search_skills and get_skill. Activates for finding skills, browsing catalogs, or extending Claude.
Searches prompts.chat for AI prompt templates by keyword or category, retrieves by ID with variable handling, and improves prompts via AI. Use for discovering or enhancing prompts.
Checks Next.js compilation errors using a running Turbopack dev server after code edits. Fixes actionable issues before reporting complete. Replaces `next build`.
@[simp], @[ext], etc.).FunLike API for morphism classes, SetLike API for subobject classes.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.s.Nonempty over alternatives. Use hne : x ≠ ⊥ in hypotheses (easier to check), hlt : ⊥ < x in conclusions (more powerful).erw, or rfl after simp/rw usually means the API is missing lemmas.The full review guide and style references: