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
6 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 trailing semicolons #41695
- chore(Algebra/Group/Action/Pointwise/Set): generalize smul_mem_smul_set_iff to IsLeftCancelSMul #42614
- feat(Algebra/Group/Action/Pointwise/Set/Basic): `mul_mem_smul_set` #42646
No open pull requests.
9 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
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
10 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
10 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
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
- chore(Algebra/Order/BigOperators): follow the `₀` naming convention #39692
- 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
4 open pull requests
9 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(Order/WithBot): remove defeq between `WithBot.LE`/`LT` and `WithTop.LE`/`LT` #42622
- 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(MeasureTheory/MeasurableSpace/Constructions): remove some defeq abuse #40648
- chore: tag some measurability lemmas with `fun_prop` #43187
- feat(MeasureTheory): measurability of a function defined by `ite` #43291
14 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
- feat(Topology/Algebra/InfiniteSum): Generalize ENNReal lemmas #38489
- 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
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43073
4 open pull requests
6 open pull requests
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- feat(MeasureTheory/Measure/ProbabilityMeasure): add toProbabilityMeasure and basic API #39588
- 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
7 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
8 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
- chore: remove declarations deprecated between 2021-08-11 and 2026-02-11 #42655
3 open pull requests
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.