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.

PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support

No open pull requests.

PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics

3 open pull requests

• chore: use `open scoped` #4960
  merge-conflict, awaiting-CI
• feat: generalize isLittleO_const_id_atTop/atBot #12192
  merge-conflict, awaiting-author, t-analysis
• chore: attribute [induction_eliminator] #12605
  merge-conflict, awaiting-author

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic

6 open pull requests

• chore: change some `linarith`s to `linear_combination`s #18841
  merge-conflict, WIP
• feat(Tactic/Push): add basic tags and tests #29000
  merge-conflict, blocked-by-other-PR, t-meta
• feat: new `isolate` tactic #29982
  large-import, t-meta
• Lean pr testing 11156 #31587
  merge-conflict, WIP
• chore: replace long terminal `rw […]`:s (≥4 lemmas) with bare `simp`:s #36774
• feat(Analysis/Complex): prove Jensen's inequality for the number of zeros #36950
  t-analysis

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults

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.