ℹ [8558/8564] Replayed Research.Basic
info: Research/Basic.lean:40:0: Erdos796.Statement : Prop
⚠ [8560/8564] Replayed Research.CoreSidon
warning: Research/CoreSidon.lean:82:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/CoreSidon.lean:92:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [8562/8564] Built Research.FiberTypes (5.1s)
✔ [8563/8564] Built Research (3.3s)
Build completed successfully (8564 jobs).
PASS: authored sources are placeholder-free and Lean accepts the project
