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
4 open pull requests
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
6 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
- feat(Data/Finset): `insert a (s.erase a) = insert a s` #40775
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
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- refactor: turn `Set` into a 1-field structure #39211
- refactor(Data): make `Set` a one-field structure #41506
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
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- 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
- style: add missing spaces #41942
No open pull requests.
5 open pull requests
6 open pull requests
- fix(fun_prop): do not unfold semireducible definitions in the presence of projections #35548
- feat(Dynamics): pointwise ergodic theorem (via maximal inequality) #40178
- chore: remove redudant `nonrec`'s #41259
- chore: add missing `to_additive` docstrings #41628
- chore: add missing `to_additive` docstrings in MeasureTheory.Group #41639
- feat(Dynamics): pointwise birkhoff theorem #42078
6 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
4 open pull requests
4 open pull requests
3 open pull requests
12 open pull requests
- chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) #6777
- 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
- chore(Order): infer `toDecidable*` in `*LinearOrder`s when possible #39908
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- refactor: notation for `EventuallyEq` on `Set` #41533
4 open pull requests
4 open pull requests
6 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
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.