✔ [8558/8563] Built BCZReduction.Erdos769 (4.3s)
⚠ [8559/8563] Built BCZReduction.AsymptoticBound (5.0s)
warning: BCZReduction/AsymptoticBound.lean:83:2: 'norm_num only [Nat.cast_mul, Nat.cast_pow]' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: BCZReduction/AsymptoticBound.lean:130:50: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8560/8563] Built BCZReduction.CutoffBridge (4.1s)
✔ [8561/8563] Built BCZReduction.DisproofReduction (3.0s)
✔ [8562/8563] Built BCZReduction (3.7s)
Build completed successfully (8563 jobs).
