Upstreaming dashboard
Files ready to upstream
The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.
No open pull requests.
8 open pull requests
- chore: change some `linarith`s to `linear_combination`s #18841
- feat(Tactic/Push): add basic tags and tests #29000
- feat: new `isolate` tactic #29982
- Lean pr testing 11156 #31587
- feat(Tactic/Positivity): make positivity work for types that are not partial orders #35394
- chore: replace long terminal `rw […]`:s (≥4 lemmas) with bare `simp`:s #36774
- chore: golf using .ne and friends #37553
- test: insert `@[informal]` attributes from overview #38195
5 open pull requests
- chore(*): turn comments before declarations into docstrings #36635
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- feat(NumberTheory): Chebyshev's lower bound on primorial #37299
- feat: also check for norm_num in the flexible linter #37671
- feat: linters for recommended field_simp style, rebased #38000
No open pull requests.
Files easy to unlock
The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.