'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'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]
RegularityRadius.lean:683: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]
'RegularityConstant.lipschitz_on_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.equicontinuous_from_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.compl_real_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.two_stage_compl_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.amp_lt_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.amp_lt_one_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.window_radius_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.Keta_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.expectation_eta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.equicontinuous_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
