Upstreaming dashboard
This page is generated automatically by the
leanprover-community/upstreaming-dashboard-action
during CI. It surveys CombinatorialRigidity/Mathlib/ — the mirror
directory for upstream-eligible lemmas (see
DESIGN.md)
— and reports what has and hasn’t been upstreamed yet.
Upstreaming dashboard
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.
No open pull requests.
1 open pull request
1 open pull request
3 open pull requests
8 open pull requests
- feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title #26013
- feat(Tactic/Push): add basic tags and tests #29000
- feat: remove `Membership` instance for `SetLike` #34473
- chore(Data/Finset/Card): rename `pred_card_le_card_erase` to `sub_one_card_le_card_erase` #36832
- chore: remove simple `nonrec` occurences #41276
- chore: remove redudant `have`'s #41749
- chore: avoid `Subrelation` where possible #43287
- chore: use Nat.pred in Finset.pred_card_le_card_erase #43508
3 open pull requests
No open pull requests.
5 open pull requests
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- feat: extend the `whitespace` linter to proof bodies #30658
- refactor: remove `DecidableEq` and `DecidableLT` from `LinearOrder` #42577
- feat(LinearAlgebra/ExteriorPower): generators of the exterior powers #43081
- feat(Data/Finset/Sort): add filtering and greatest insertion lemmas #44941
4 open pull requests
4 open pull requests
- chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) #27399
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by `|V|` #43953
- feat(Linter): terminal cdot linter using `tacticAnalysis` #44737
5 open pull requests
- chore(Data/Finset/Card): rename `pred_card_le_card_erase` to `sub_one_card_le_card_erase` #36832
- chore(Data/Set/Finite/Basic): fix `Fintype ({a} : Set α)` instance #38870
- feat(ModelTheory): add counting formulas #42025
- feat(ModelTheory/ElementaryMaps): preserve definable-set cardinality #42026
- feat(SimpleGraph/Connectivity/EdgeConnectivity): morphism lemmas for edge reachability/connectivity #43823
No open pull requests.
13 open pull requests
- feat: extend the `whitespace` linter to proof bodies #30658
- feat(Data/Set): add `Set.diag` #38380
- chore: replace `by exact` occurences #40223
- feat(Combinatorics/SimpleGraph/Paths): some lemmas about inducing walks #40967
- chore: replace `simp_all` with `simp` whenever possible #41896
- refactor: rename the `diag` name token to `diagonal` #43494
- feat: a syntax linter for the `@[congr]` attribute #43692
- feat(Data/Sym/Sym2): `Sym2.map` lifts equivalences #43815
- feat(SimpleGraph/Connectivity/Connected): define `IsBridgeless` #43821
- chore(Data/Sym/Sym2): infer `Std.Symm` in `Sym2.fromRel` #43892
- chore: fix more congruence lemmas #44093
- feat(Linter): terminal cdot linter using `tacticAnalysis` #44737
- chore: rename `notation3` to `notation +delab` #45028
No open pull requests.
4 open pull requests
1 open pull request
No open pull requests.
5 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.