✔ [8558/8567] Built ConditionalNegation.Erdos769 (4.3s)
⚠ [8559/8567] Built ConditionalNegation.AsymptoticBound (5.5s)
warning: ConditionalNegation/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: ConditionalNegation/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/8567] Built ConditionalNegation.CutoffBridge (4.2s)
✔ [8561/8567] Built ConditionalNegation.Grid (6.7s)
✔ [8562/8567] Built ConditionalNegation.DisproofReduction (4.1s)
⚠ [8563/8567] Built ConditionalNegation.Substitution (5.2s)
warning: ConditionalNegation/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: ConditionalNegation/Substitution.lean:149:61: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8564/8567] Built ConditionalNegation.RegularSemigroup (4.1s)
warning: ConditionalNegation/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: ConditionalNegation/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: ConditionalNegation/RegularSemigroup.lean:48:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8565/8567] Built ConditionalNegation.BCZConsequence (4.4s)
✔ [8566/8567] Built ConditionalNegation (3.7s)
Build completed successfully (8567 jobs).
