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.Module.PositiveLinearMap

1 open pull request

• chore: remove declarations deprecated between 2021-03-15 and 2025-09-15 #36666
  new-contributor, merge-conflict

LeanOA.Mathlib.Algebra.Order.Star.Basic

2 open pull requests

• feat: modify `cfc_tac` to use `grind` #27829
  merge-conflict, WIP
• chore: remove declarations deprecated between 2021-03-15 and 2025-09-15 #36666
  new-contributor, merge-conflict

LeanOA.Mathlib.Algebra.Star.StarAlgHom

7 open pull requests

• refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
  t-algebra, awaiting-author, merge-conflict
• experiment: how many `inferInstanceAs` can be replaced with `inferInstanceAs%` (#36420 version) #36515
  WIP, merge-conflict
• experiment: `rm_set_option.py` after greedily deploying #35950's `inferInstanceAs%` #36573
  large-import, merge-conflict
• experiment: `rm_set_option.py` after greedily deploying #36420's `inferInstanceAs%` #36578
  merge-conflict
• chore: remove declarations deprecated between 2021-03-15 and 2025-09-15 #36666
  new-contributor, merge-conflict
• chore: override `npow` in compositional monoids #36878
• chore: bump toolchain to `v4.29.0-rc7` #37034

LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit

1 open pull request

• feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball #36327
  t-analysis, blocked-by-other-PR

LeanOA.Mathlib.Analysis.CStarAlgebra.Basic

2 open pull requests

• chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` #26912
  merge-conflict, t-algebra
• chore: do not use `inf` `sup` in `LinearOrder` lemmas #35881
  t-order, blocked-by-other-PR

LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

1 open pull request

• feat: transfer instances of `ContinuousFunctionalCalculus` to type synonyms with weaker topologies #35605
  merge-conflict, t-analysis

LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

6 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
• feat: `GroupWithZero` versions of `le` lemmas #34120
  WIP, large-import, merge-conflict
• experiment: `rm_set_option.py` after greedily deploying #36420's `inferInstanceAs%` #36578
  merge-conflict
• feat(CStarAlgebra): `Ring.inverse` is convex and antitone on strictly positive operators #37009
  t-analysis

LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs

No open pull requests.

LeanOA.Mathlib.Analysis.CStarAlgebra.MulNonneg

No open pull requests.

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
• chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
  delegated
• chore: fix diamonds for Real/Complex Algebra instances #36087
  blocked-by-other-PR
• chore: deprecate `push_neg` #36392
  t-meta

LeanOA.Mathlib.Analysis.Convex.Extreme

1 open pull request

• fix: deduplicate variables #6079
  merge-conflict, awaiting-CI

LeanOA.Mathlib.Analysis.RCLike.ContinuousMap

1 open pull request

• feat(Analysis/RCLike): lifting `C(X, ℝ)` to `C(X, 𝕜)` #36999
  t-analysis

LeanOA.Mathlib.Analysis.RCLike.Extend

1 open pull request

• chore: cont -> continuous_toFun #33561
  merge-conflict

LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

4 open pull requests

• feat: modify `cfc_tac` to use `grind` #27829
  merge-conflict, WIP
• feat: preliminary `grind` tags for `IsUnit` #28132
  merge-conflict, t-algebra
• feat: add `IsSemitopologicalRing` #36617
  t-topology, t-algebra
• feat(CStarAlgebra): `Ring.inverse` is convex and antitone on strictly positive operators #37009
  t-analysis

LeanOA.Mathlib.Misc

1 open pull request

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

LeanOA.Mathlib.Order.Hom.Basic

4 open pull requests

• refactor(CategoryTheory/MorphismProperty): some clean-ups #10349
  merge-conflict, t-category-theory
• feat(Order/FunLike): define `PointwiseLE` #10721
  merge-conflict, t-order, t-logic
• chore: get rid of generic hom coercions #21031
  WIP
• feat: replace `IsWellFounded` with `WellFounded` #35602
  t-data

LeanOA.Mathlib.Topology.Bornology.Basic

1 open pull request

• feat: define `UnboundedSpace` #7903
  merge-conflict, help-wanted, t-topology

LeanOA.Mathlib.Topology.ContinuousMap.Bounded.Normed

3 open pull requests

• feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball #36327
  t-analysis, blocked-by-other-PR
• feat: norm of sums of continuous functions whose product is zero #36407
  t-topology, delegated
• feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements #36416
  blocked-by-other-PR

LeanOA.Mathlib.Topology.Order.LeftRightNhds

1 open pull request

• chore: migrate to `tfae` block tactic #11003
  merge-conflict, WIP, blocked-by-other-PR, t-meta

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.