Upstreaming dashboard

The eventual goal of the LeanCamCombi project is to not contain any significant new formalisation, but instead to act as a shallow layer over Mathlib showing concretely how to turn paper-combinatorics into Lean-combinatorics.

As such, it is crucial to continuously organise upstreaming from LeanCamCombi to Mathlib. The way we organise this is with the following two lists, showing files with no LeanCamCombi 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.

LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM

2 open pull requests

• feat: extend the `whitespace` linter to proof bodies #30658
  large-import, t-linter
• perf: test the effect of localizing the whitespace linter #34086
  large-import, merge-conflict

LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density

1 open pull request

• refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API #4127
  merge-conflict, awaiting-author, t-combinatorics

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.

LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup

7 sorries