LargeFieldSupply.lean:65:6: warning: Variable name `s` 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] _s

Note: This linter can be disabled with `set_option linter.unusedVariables false`
LargeFieldSupply.lean:65:8: warning: Variable name `v` 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] _v

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'LargeFieldSupply.supply_union' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.phi_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.fixed_angle_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.supply_anti_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.block_mgf_indep' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.block_mgf_holder' depends on axioms: [propext, Classical.choice, Quot.sound]
