Upstreaming dashboard
The eventual goal of the APAP project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from APAP to Mathlib.
The way we organise this is with the following two lists,
showing files with no APAP dependencies depending on whether they contain sorry or not.
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.
9 open pull requests
- chore: use `open scoped` #4960
- chore: dedent `to_additive` docstrings #28298
- chore(Mathlib): replace `=>` by `↦` #28622
- experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid #29605
- chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` #31949
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore: shake --keep-implied --keep-prefix --fix #39386
- chore: remove many redundant imports #41222
- perf( Mathlib/CategoryTheory/Sites/LocallySurjective.lean): investigate removing transitive import #41406 #41411
7 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- refactor: rename `MulAction` to `MonoidAction` #32737
- feat(Combinatorics/Schnirelmann): prove Mann's theorem #38077
- chore: remove declarations deprecated between 2021-06-15 and 2025-12-15 #40618
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data): rename `setOf` to `Set.ofPred` #41507
- chore: remove trailing semicolons #41695
10 open pull requests
- ignore this: Lean pr testing 9124 #26581
- chore: fix naming of `mono` and `monotone` #26911
- chore: dedent `to_additive` docstrings #28298
- feat(Tactic/Push): add basic tags and tests #29000
- refactor (Algebra.Group.Defs): add npow/zpow/nsmul/zsmul as fields of new parents classes #29482
- experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid #29605
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- refactor: rename `MulAction` to `MonoidAction` #32737
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data): rename `setOf` to `Set.ofPred` #41507
No open pull requests.
No open pull requests.
No open pull requests.
6 open pull requests
- feat: define the additive submonoid of positive elements in a star ordered ring #4871
- chore: fix links #27709
- feat: modify `cfc_tac` to use `grind` #27829
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- test: insert `@[informal]` attributes from overview #38195
- feat: ℕ+ powers in semigroups #40785
4 open pull requests
6 open pull requests
- lint also `let` vs `have` #12181
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat: add convolution_comp_add_right #32169
- chore: golf using .ne and friends #37553
- test: insert `@[informal]` attributes from overview #38195
- feat(Analysis/Convolution): add convolution_symm, convolution, (3 more lemmas) #41557
5 open pull requests
12 open pull requests
- refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` #6931
- chore: migrate to `tfae` block tactic #11003
- feat: more linting of cdots #12411
- feat: a norm_num extension for complex numbers #26975
- chore: reduce `Topology` imports in `Data` #29012
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(RCLike): add `Continuous.re` and similar #34419
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- fix(Tactic/Continuity): mark Continuous.comp' as unsafe #36806
- chore(Data/Real): encapsulate real numbers #38702
- chore(Analysis/RCLike/Basic): state norm_I with positive polarity #41585
10 open pull requests
- feat: port ge_or_gt linter from mathlib3 #12879
- chore: replace some use of > or ≥ by < or ≤ #12933
- chore: split Mathlib.Algebra.Star.Basic #14330
- feat: a norm_num extension for complex numbers #26975
- chore: fix links #27709
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(Data/Real): encapsulate real numbers #38702
- feat(Data/Complex/Basic): add simproc to reduce powers of I #39506
- feat: ℕ+ powers in semigroups #40785
11 open pull requests
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- feat: extend the `whitespace` linter to proof bodies #30658
- perf: test the effect of localizing the whitespace linter #34086
- feat: `GroupWithZero` versions of `le` lemmas #34120
- refactor: use `OrderSupInfSet` #35263
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- chore(Data/Real): encapsulate real numbers #38702
- feat(Algebra/Order/Nonneg): add `Nonneg` for nonnegative subtype #41134
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
7 open pull requests
- feat: add wrap_instance% using core's wrapInstance #37073
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore: remove redundant `unfold`s #39029
- feat(Data/ZMod/Basic): isUnit characterisation in prime power moduli #40005
- feat(Data/ZMod/Basic): idempotents in ZMod (p^d) are exactly {0, 1} #40006
- feat(ModularForm): add eisensteinSeries G_k^v #41613
- feat(Data/ZMod): add `Unique (ZMod 2)ˣ` instance #41742
No open pull requests.
9 open pull requests
- feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) #20372
- WIP: generalise lemmas to ENorm #21375
- chore: change more lemmas to be about enorm instead of nnnorm #21433
- chore: make `finiteness` a default tactic #26090
- chore: more enorm lemmas #27446
- refactor: unbundle algebra from `ENormed*` #28803
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- refactor: redefine `eLpNorm` at `p = 0` #39311
- chore: replace `by calc` by `calc` whenever possible #40292
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.