breen_deligne refactor

Stream: condensed mathematics

[Johan Commelin]

I'm refactoring a bunch of stuff in breen_deligne/* to make it easier to prove things about the homotopy.
Going to bed now. Pushed my wip to bd_refactor.
There were some sorries in those files (on master) but it probably doesn't make sense to work on those, until the refactor is done.

[Johan Commelin]

This refactor is now done, and merged into master.

[Johan Commelin]

At some point we'll need some constants c_ c' : nat -> nnreal that play well with breen_deligne.eg.
Here eg is the explicit example of breen_deligne.package, see breen_deligne/eg.lean.

What we need is that for variable r r' : nnreal (satisfying [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' ≤ 1)]) we have

• eg.very_suitable r r' c_ (so c_ shall depend on r and r')
• eg.adept c_ c' (so c' shall be constructed in terms of a c_, here r and r' don't play a role)

[Johan Commelin]

So, if you like playing with division/inverses of non-negative reals, then feel free to add constructions of such sequences to eg.lean.