LatticeGaugeQuarticRowColumnBound.lean:107:48: warning: Variable name `hc` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hc

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'LatticeGauge.QuarticRowColumn.weighted_quartic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticRowColumn.row_quartic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticRowColumn.schur_quartic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticRowColumn.representative_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticRowColumn.cone_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticRowColumn.cone_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
