Def Mathlib.Tactic.SolveByElim.Config.introsAfter

Modification history

2024-01-05 01:23

Mathlib/Tactic/SolveByElim.lean

chore: bump std4 dependency (#9426) …

Deleted Mathlib.Tactic.SolveByElim.Config.introsAfter View on Github →

2023-04-18 12:01

Mathlib/Tactic/SolveByElim.lean

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

Added Mathlib.Tactic.SolveByElim.Config.introsAfter View on Github →