Commit 2025-11-25 05:16 024965e5

View on Github ā†’

chore: delete Mathlib.Tactic.Propose (#32083) See zulip: #mathlib4 > "test mathlib" step is slow in CI @ šŸ’¬.

  • Delete Mathlib/Tactic/Propose.lean - the have? forward reasoning search tactic
  • Remove associated test file MathlibTest/propose.lean
  • Remove all imports and references from Mathlib.lean, Mathlib/Tactic.lean, Mathlib/Tactic/Common.lean, Mathlib/Tactic/Linter/UnusedTacticExtension.lean, and scripts/nolints.json šŸ¤– Generated with Claude Code

Estimated changes

deleted def bar
deleted theorem dvd_of_dvd_pow