Upstreaming dashboard
The eventual goal of the PFR project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from PFR to Mathlib.
The way we organise this is with the following two lists,
showing files with no PFR 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.
6 open pull requests
- chore: dedent `to_additive` docstrings #28298
- chore(Mathlib): replace `=>` by `↦` #28622
- chore: golf using .ne and friends #37553
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- chore: shake --keep-implied --keep-prefix --fix #39386
- refactor: replace bundled commutative classes by `IsMulCommutative` (experiment) #44466
6 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- feat(Combinatorics/Schnirelmann): prove Mann's theorem #38077
- chore: remove trailing semicolons #41695
- feat(Algebra/Group/Action/Pointwise/Set/Basic): `mul_mem_smul_set` #42646
- refactor: rename `MulAction` to `MonoidAction` #43404
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
No open pull requests.
1 open pull request
4 open pull requests
14 open pull requests
- feat: grind tags for set operations #27683
- feat(Tactic/Push): add basic tags and tests #29000
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- bench: lean4#10832 #30642
- bench: before lean4#10832 #30643
- (WIP) Separation axioms #32865
- chore: tag set lemmas with @[push] #38853
- refactor: turn `Set` into a 1-field structure #39211
- feat: use `max`/`min` for `union`/`inter` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- feat: `@[gcongr]` for `eq_top_mono` and friends #44334
- chore: golf using new `@[gcongr]` lemmas #44335
- chore: adaptations for stronger `simpNF` - part 1 #44554
- feat(RingTheory/MvPolynomial/Groebner): add division with weak reduction #45208
6 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- bench: lean4#10832 #30642
- bench: before lean4#10832 #30643
- refactor: turn `Set` into a 1-field structure #39211
- feat: use `max`/`min` for `union`/`inter` in `Set`, `Finset`, `ZFSet`, `Class` #42316
8 open pull requests
- 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
- chore: replace `simp_all` with `simp` whenever possible #41896
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- feat: char two API (WIP) #43575
- refactor: unify `CharZero` with `CharP` #44761
No open pull requests.
5 open pull requests
5 open pull requests
- feat(Data/Set): add `Set.diag` #38380
- chore: remove redudant `nonrec`'s #41259
- chore: add missing `to_additive` docstrings #41628
- feat(Dynamics): pointwise ergodic theorem for normed spaces #42078
- fix(MeasureTheory/Group/Arithmetic): make `Finset.measurable_prod` state the product of functions #44812
7 open pull requests
- wip, chore: rename Directed -> Predirected [please-adopt] #38792
- chore: replace `by calc` by `calc` whenever possible #40292
- chore(MeasureTheory): remove all `erw` in `MeasureTheory` #40348
- chore(MeasureTheory/Integral/Lebesgue/Basic): fix an `erw` #40392
- chore: prefer `beta_reduce` over `(d)simp only` #41933
- chore: rename Directed to Predirected #42290
- chore: rename `notation3` to `notation +delab` #45028
5 open pull requests
1 open pull request
9 open pull requests
- refactor: disable `simp` in `measurability` #30966
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- feat(Data/Set): add `Set.diag` #38380
- chore(MeasureTheory/MeasurableSpace/Constructions): remove defEq abuse #40425
- chore: tag some measurability lemmas with `fun_prop` #43187
- refactor: rename the `diag` name token to `diagonal` #43494
- feat({Topology,MeasureTheory}): instances for `Additive`/`Multiplicative` #45174
- feat(MeasureTheory): measurable group hom from locally compact to separable is continuous #45214
- feat: add `MeasurableSpace.prod_mono` #45231
No open pull requests.
5 open pull requests
7 open pull requests
- Docstring enumerations #28067
- refactor: disable `simp` in `measurability` #30966
- chore: specify doc-strings of auto-generated additive declarations di… #41565
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
- chore: golf using new `@[gcongr]` lemmas #44335
- chore: rename `notation3` to `notation +delab` #45028
- chore(MeasureTheory): generalize more `biUnion` lemmas to predicate-bounded unions #45148
3 open pull requests
6 open pull requests
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(MeasureTheory): remove all `erw` in `MeasureTheory` #40348
- chore(MeasureTheory/Measure/Prod): remove an `erw` #40409
- chore: replace terminal `convert` with `exact` #41762
- feat(MeasureTheory): generalize `QuasiMeasurePreserving` to `AEMeasurable` #43191
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
7 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- feat: remove `Membership` instance for `SetLike` #34473
- feat: reduce the use of Classical.choice #35685
- feat: instance diamond linter #38781
- refactor: rename Function.swap #42282
- Instancediamonds merged #44367
1 open pull request
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.