HasseWeil · projects/HasseWeil/HasseWeil/Foundation/EC/TranslateValuation.lean · declaration pointValuation_translateAlgEquivOfPoint_of_le_one starts at line 1387; its proof starts at line 1396 and spans about 90 physical lines.
Target fingerprint: 6250e0b1a770cca9
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 HasseWeil build, zero new sorries, and unchanged #print axioms.
HasseWeil·projects/HasseWeil/HasseWeil/Foundation/EC/TranslateValuation.lean· declarationpointValuation_translateAlgEquivOfPoint_of_le_onestarts at line 1387; its proof starts at line 1396 and spans about 90 physical lines.Target fingerprint:
6250e0b1a770cca9Run
/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 andHasseWeilbuild, zero new sorries, and unchanged#print axioms.