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.
10 open pull requests
- chore: use `open scoped` #4960
- feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` #19013
- feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple #19315
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat(BigOperators/Fin): Sum/product over `Fin` intervals #19697
- 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
7 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
- chore: use `congr()` much more widely #43408
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
No open pull requests.
10 open pull requests
- feat: add Qq wrappers for ToExpr #5952
- style: Change Subtype.val to (↑) #12465
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat: `Clone` and some instances #20051
- feat: Definition of `Clone` #23460
- chore: fix recursors #23489
- Post's lattice #24744
- feat: a linter for duplicated `open` #25362
- chore: rename arguments of `Nat.strong_induction_on` #41540
- chore(Data/Nat/Init): fix recursors #43848
7 open pull requests
- feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605
- chore: attribute [induction_eliminator] #12605
- feat: port ge_or_gt linter from mathlib3 #12879
- chore: replace some use of > or ≥ by < or ≤ #12933
- feat: reduce the use of Classical.choice #35685
- chore: rename Directed to Predirected #42290
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
11 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
- refactor(Data): make `Set` a one-field structure #41506
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- refactor: replace `SemilatticeSup.sup` with `max` #43472
11 open pull requests
- feat: a linter for duplicated `open` #25362
- 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
- chore(Data): refactor proofs where `grind?` fails #39808
- refactor(Data): make `Set` a one-field structure #41506
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- feat: `membership` tactic #42342
- fix: use meta imports for metaprogramming dependencies #43912
8 open pull requests
- 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
- chore: replace `simp_all` with `simp` whenever possible #41896
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- feat: char two API (WIP) #43575
No open pull requests.
9 open pull requests
- feat: more linting of cdots #12411
- feat: `GroupWithZero` versions of `le` lemmas #34120
- feat(Data/Set): add `Set.diag` #38380
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore: remove simple `nonrec` occurences #41276
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
- feat(MeasureTheory): generalize `QuasiMeasurePreserving` to `AEMeasurable` #43191
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
4 open pull requests
8 open pull requests
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- 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(MeasureTheory): generalize hypotheses to `NullMeasurableSet` #42924
5 open pull requests
- chore(MeasureTheory): use `0` instead of `const _ 0` #24060
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(MeasureTheory): remove all `erw` in `MeasureTheory` #40348
- chore: rename Directed to Predirected #42290
6 open pull requests
- style: replace preimage_val with ↓∩ notation #12418
- feat(Dynamics): Hopf decomposition #16150
- Clean up quotient APIs #16210
- feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem #17368
- chore: tag some measurability lemmas with `fun_prop` #43187
- feat(MeasureTheory): measurability of a function defined by `ite` #43291
7 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
- feat(MeasureTheory): measurability of a function defined by `ite` #43291
- refactor: rename the `diag` name token to `diagonal` #43494
12 open pull requests
- feat: more linting of cdots #12411
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- Docstring enumerations #28067
- feat: extend the `whitespace` linter to proof bodies #30658
- refactor: use `OrderSupInfSet` #35263
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- wip, chore: rename Directed -> Predirected [please-adopt] #38792
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore: remove `CovariantClass` and `ContravariantClass` #42273
- chore: rename Directed to Predirected #42290
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
4 open pull requests
5 open pull requests
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- refactor: change ProbabilityMeasure.map to not require measurability #42830
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
9 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
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
- feat(MeasureTheory): generalize `QuasiMeasurePreserving` to `AEMeasurable` #43191
- feat(Measure/Prod): add map_prod_map_of_aemeasurable #43485
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
10 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
- feat(Order/Interval/Finset/Defs): `LocallyFiniteOrder{Bot,Top}` implies `WellFounded{LT,GT}` #39427
- refactor: rename Function.swap #42282
- feat(Translate): command for adding a translation #43750
- feat(Algebra/Homology/ShortComplex/Basic): use `to_dual` #43804
- chore: clean up some `to_dual` debt #43818
3 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.