BoxFiberSiteSum.lean:22:0: warning: automatically included section variable(s) unused in theorem `BoxFiberSiteSum.fiber_swap`:
  [DecidableEq F]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq F] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
'BoxFiberSiteSum.fiber_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_site_le_fiber' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_site_le_face_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_hsite_of_fiber' depends on axioms: [propext, Classical.choice, Quot.sound]
