'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
NontreeBackground.lean:154:12: warning: Variable name `h` 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] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.nontree_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.quadratic_fields' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_stays' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.invariant_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.pointwise_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
