✔ [8558/8562] Built Substitution.Erdos769 (4.2s)
✔ [8559/8562] Built Substitution.Grid (5.5s)
⚠ [8560/8562] Built Substitution.Substitution (4.6s)
warning: Substitution/Substitution.lean:149:21: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Substitution/Substitution.lean:149:61: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8561/8562] Built Substitution (3.6s)
Build completed successfully (8562 jobs).
