⚠ [8558/8560] Built OddGridGCD.Basic (8.3s)
warning: OddGridGCD/Basic.lean:67:39: Variable name `hM` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: OddGridGCD/Basic.lean:69:45: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: OddGridGCD/Basic.lean:69:45: 'omega' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: OddGridGCD/Basic.lean:201:37: Try `simp at hroot` instead of `simpa using hroot`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [8559/8560] Built OddGridGCD (3.6s)
Build completed successfully (8560 jobs).
