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.

LeanOA.Mathlib.Algebra.Order.Star.Basic

1 open pull request

• feat: modify `cfc_tac` to use `grind` #27829
  merge-conflict, WIP

LeanOA.Mathlib.Algebra.Star.StarProjection

No open pull requests.

LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

3 open pull requests

• test: refactor in CI #15679
  merge-conflict, WIP
• perf: reorder `extends` and remove some instances in algebra hierarchy #16594
  merge-conflict, slow-typeclass-synthesis, t-algebra
• feat: preliminary `grind` tags for `IsUnit` #28132
  merge-conflict, t-algebra

LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs

No open pull requests.

LeanOA.Mathlib.Analysis.CStarAlgebra.MulNonneg

No open pull requests.

LeanOA.Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

2 open pull requests

• refactor: deprecate `ContinuousLinearMapClass` #33448
  t-topology, t-algebra, awaiting-author
• refactor: deprecate `LinearIsometryClass` #33450
  t-algebra, t-analysis, blocked-by-other-PR, t-topology, merge-conflict

LeanOA.Mathlib.Analysis.CStarAlgebra.Projection

1 open pull request

• feat: equivalent conditions for `p ≤ q` for projections in a C⋆-algebra #35204
  t-analysis, large-import

LeanOA.Mathlib.Analysis.Complex.Basic

8 open pull requests

• feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance #6210
  merge-conflict, WIP, t-algebra, t-analysis
• refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields #9642
  WIP, merge-conflict, awaiting-author, help-wanted, t-analysis
• feat(Data/Complex/Exponential): prove some useful results about the complex exponential. #20313
  merge-conflict, t-analysis, new-contributor
• chore: fix links #27709
  merge-conflict, WIP
• chore: add a computable shortcut for `AddCommMonoid ℂ` #29615
  t-analysis, easy, bench-after-CI
• chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
  delegated, awaiting-CI
• chore: golf proofs #35189
• style: fix many leading by's in mathlib #35343

LeanOA.Mathlib.Analysis.RCLike.Extend

3 open pull requests

• chore: cont -> continuous_toFun #33561
  merge-conflict
• refactor: improve API connecting `ℝ`- and `𝕜`-linear functionals #34543
  t-analysis
• feat: continuous linear equivalence between continuous `ℝ`- and `𝕜`-linear functionals, when equipped with the weak⋆-topology #34728
  t-analysis, blocked-by-other-PR

LeanOA.Mathlib.LinearAlgebra.Complex.Module

1 open pull request

• refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
  t-algebra, awaiting-author, merge-conflict

LeanOA.Mathlib.Misc

1 open pull request

• Development branch (1) #30122
  WIP, large-import, merge-conflict

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.