BernoulliRegular · projects/FltRegularBernoulli/BernoulliRegular/Reflection/Local/ComponentDimension/CharacterProjectionFinrankOne.lean · declaration completedPrincipalUnitModPEigenspace_mem_filtration_succ_of_exists_pow_ne starts at line 105; its proof starts at line 112 and spans about 87 physical lines.
Target fingerprint: 0fa3996ad94976cf
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/Local/ComponentDimension/CharacterProjectionFinrankOne.lean· declarationcompletedPrincipalUnitModPEigenspace_mem_filtration_succ_of_exists_pow_nestarts at line 105; its proof starts at line 112 and spans about 87 physical lines.Target fingerprint:
0fa3996ad94976cfRun
/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.