Proved solution

This module imports the full proof development. The three declarations named in comparator.json,

• Nikodym.card_compl_pow_mul_card_le,
• Nikodym.card_ge_pow_sub,
• Nikodym.exists_isNikodym_card_le,

are proved in Nikodym/Main.lean (with the same names and statements as in Challenge.lean) and are therefore present in this module's environment. Comparator checks that each one has exactly the same statement as its counterpart in Challenge.lean, that the definition Nikodym.IsNikodym appearing in those statements is identical in both modules, and that the proofs use only the axioms propext, Classical.choice, and Quot.sound.

The examples below are a readable local witness of the same facts: they type-check only if the proved theorems have the advertised types.