lean-module-compile-recovery

name	lean-module-compile-recovery
description	Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
domain	lean-proof-maintenance
confidence	high
source	earned

Context

Use this when a single Lean module has many local type-mismatch failures caused by over-strong endpoint equalities that are not derivable from available assumptions, and the goal is to restore compilation safely.

Patterns

• Keep namespace and declaration names stable; prefer codomain weakening over deleting declarations.
• For brittle Path/RwEq endpoints on abstract carriers, switch to reflexive witnesses (Path.refl _, RwEq.refl _) when no lawful proof source exists.
• If structure-level extensional equalities are disproportionately expensive, temporarily degrade specific theorems to True in targeted rescue passes.
• Rebuild only the target module first (lake build <Module>) to confirm the fix is scoped.
• For OmegaGroupoid-derived cells, mirror source universes exactly (Derivation₂/Derivation₃ live in Type (u + 2)), or wrappers/structures will fail with universe and missing-field cascades.
• Apply higher-cell constructors with explicit endpoints when required (e.g., MetaStepHigh.diamond_filler (n := n) c₁ c₂), not as unapplied constants.
• In HoTT modules using Equivalences.Equiv, prefer ≃ₚ with toFun/isEquiv.inv/sect/retr; avoid unavailable core identifiers like _root_.Equiv and Function.Bijective.
• theorem declarations must be proposition-valued: when available evidence is Path ..., convert witnesses via .toEq at theorem boundaries.

Examples

• ComputationalPaths/Stable/HomotopyGroups.lean:
  • converted selected non-derivable equalities to reflexive Path/RwEq;
  • downgraded SpectrumHom.comp_id and SpectrumHom.id_comp to True;
  • validated with & "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Stable.HomotopyGroups.
• ComputationalPaths/Path/OmegaGroupoid/TruncationProof.lean:
  • changed local Type u wrappers over Derivation₂/Derivation₃ to Type (u + 2);
  • instantiated MetaStepHigh.diamond_filler with explicit n, c₁, c₂;
  • validated with & "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Path.OmegaGroupoid.TruncationProof.
• ComputationalPaths/Path/HoTT/Descent.lean:
  • replaced brittle equivalence notation/identifiers with ≃ₚ-compatible usage;
  • converted theorem-facing path witnesses to proposition-level equalities via .toEq;
  • replaced unavailable circle loop reference with Pushouts.Circle.loop;
  • validated with & "$env:USERPROFILE\.elan\bin\lake.exe" build ComputationalPaths.Path.HoTT.Descent.

Anti-Patterns

• Do not introduce axioms or sorry to silence failures.
• Do not perform broad cross-module rewrites when a local codomain weakening resolves the blocker.
• Do not change import-hub wiring or unrelated files during targeted module rescue.