BernoulliRegular · projects/FltRegularBernoulli/BernoulliRegular/Reflection/WeakSplitting/UniformResidueDegree.lean · declaration idealNormMultiplicity_prime_pow_mul_d_eq_card_sym_of_uniform starts at line 212; its proof starts at line 217 and spans about 61 physical lines.
Target fingerprint: 2fbaf946922ca4fb
Run /decompose-proof on this one sorry-free proof. Preserve the top-level declaration statement byte-for-byte. Search mathlib and the full repository before extracting helpers; use existing APIs where possible. Extract genuinely reusable or named mathematical steps, split branches longer than 10 lines, leave the main proof under 15 lines, and leave no proof over 50 lines. Keep helper statements appropriately scoped and mathlib-named. Add no sorry/admit. Verify the target module and BernoulliRegular build, zero new sorries, and unchanged #print axioms.
BernoulliRegular·projects/FltRegularBernoulli/BernoulliRegular/Reflection/WeakSplitting/UniformResidueDegree.lean· declarationidealNormMultiplicity_prime_pow_mul_d_eq_card_sym_of_uniformstarts at line 212; its proof starts at line 217 and spans about 61 physical lines.Target fingerprint:
2fbaf946922ca4fbRun
/decompose-proofon this one sorry-free proof. Preserve the top-level declaration statement byte-for-byte. Search mathlib and the full repository before extracting helpers; use existing APIs where possible. Extract genuinely reusable or named mathematical steps, split branches longer than 10 lines, leave the main proof under 15 lines, and leave no proof over 50 lines. Keep helper statements appropriately scoped and mathlib-named. Add nosorry/admit. Verify the target module andBernoulliRegularbuild, zero new sorries, and unchanged#print axioms.