✔ [8558/8564] Built RegularSemigroup.Erdos769 (4.1s)
✔ [8559/8564] Built RegularSemigroup.CutoffBridge (4.2s)
✔ [8560/8564] Built RegularSemigroup.Grid (5.8s)
⚠ [8561/8564] Built RegularSemigroup.Substitution (4.5s)
warning: RegularSemigroup/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: RegularSemigroup/Substitution.lean:149:61: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8562/8564] Built RegularSemigroup.RegularSemigroup (3.9s)
warning: RegularSemigroup/RegularSemigroup.lean:29:25: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8563/8564] Built RegularSemigroup (3.4s)
Build completed successfully (8564 jobs).
