Def Mathlib.Tactic.Propose.solveByElim

Modification history

2025-11-25 05:16

Mathlib/Tactic/Propose.lean

chore: delete `Mathlib.Tactic.Propose` (#32083) …

Deleted Mathlib.Tactic.Propose.solveByElim View on Github →

2023-04-18 12:01

Mathlib/Tactic/Propose.lean

feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) …

Added Mathlib.Tactic.Propose.solveByElim View on Github →