Reach proof elaboration breaks across Lean toolchain compatibility boundary
Reach exposes its proof interfaces as Lean 4 library code backed by elaborators and tactics, so each release is pinned to a specific Lean toolchain. When a project upgrades its Lean toolchain but keeps the same Reach checkout—or updates Reach without moving the pinned toolchain—previously working tactic-based proofs can fail to elaborate. The tactic and help