'SharpWindow.sharp_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.lipschitz_form_implies_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.maps_ball_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.lipschitz_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta28_tau1' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.margin_beta28_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta20_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta16_tau1_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
SharpWindow.lean:143:0: warning: automatically included section variable(s) unused in theorem `EntireCopy.pull_succ'`:
  [MetricSpace X]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [MetricSpace X] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
SharpWindow.lean:154:0: warning: automatically included section variable(s) unused in theorem `EntireCopy.pull_mem`:
  [MetricSpace X]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [MetricSpace X] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
'SharpWindow.sharp_entire_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
