Commit 2023-01-19 22:25 27c3fc8d

View on Github →

feat: solve_by_elim using (attributes) (#1581)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/Nontriviality/Core.lean

Modified Mathlib/Tactic/SolveByElim.lean

modified def Mathlib.Tactic.SolveByElim.mkAssumptionSet

added def Mathlib.Tactic.SolveByElim.parseUsing

Created Mathlib/Tactic/TagAttr.lean

added def Mathlib.Tactic.TagAttr.mkTagAttr

added def Mathlib.Tactic.TagAttr.mkTagExt

added def Mathlib.Tactic.TagAttr.registerTagAttr

added def Mathlib.Tactic.TagAttr.tagged

Modified test/solve_by_elim/basic.lean

added theorem le_rfl