ℹ [8558/8566] Replayed Research.Basic
info: Research/Basic.lean:40:0: Erdos796.Statement : Prop
⚠ [8560/8566] 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/8566] Replayed Research.FiberTypes
warning: Research/FiberTypes.lean:57:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:78:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:98:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [8564/8566] Built Research.Profile40 (31s)
✔ [8565/8566] Built Research (3.1s)
Build completed successfully (8566 jobs).
PASS: authored sources are placeholder-free and Lean accepts the project
