Yakov Pechersky

I don't think that makes sense though, because here is the reference: > PT_02_00 |   `[O,S,Se,Te;X1:1]=[Cz1H0:2][C:5]=[C:6][CX4z0,NX3:3][#1:4]>>[#1:4][O,S,Se,Te;X2:1][Cz1:2]=[C:5][C:6]=[Cz0,N:3]` Reference: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8459712/ If it was that tautomerization, I would expect to see

Yes, ditto.

I'm not very familiar with the codebase, but here are the rules: ``` std::make_tuple( std::string("1,5 (thio)keto/enol f"), std::string("[CX4z0,NX3;!H0]-[C]=[C][Cz1H0]=[O,S,Se,Te;X1]"), std::string(""), std::string("")), std::make_tuple(std::string("1,5 (thio)keto/enol r"), std::string("[O,S,Se,Te;X2!H0]-[Cz1H0]=[C]-[C]=[Cz0,N]"), std::string(""), std::string("")), ``` I don't see...

Is it possible that the 1,5 rule is combining with the 1,3 rule, making it go like the following? ``` alpha-beta unsat keto --[1,5 rule]--> beta-gamma unsat enol --[1,3 rule]-->...

Or perhaps we should supply the transform to a modified `createVolumeIsosurfaceMesh`?

I can remove the "reading" change, but currently, the existing implementation on master gets the `resNumCol` preferentially from `auth_seq_id` as it is. Why is it not preferrable to be consistent...

The reference to label_seq_id ends up, when following the parent data, referring to polymers. Which according to the molstar developers means that HETATM like entries like small molecules don't have...

OK, seems to me like whatever spec I can reference, instead there is a "common law" of how it is meant to be used. In any case, since we label...

> Have you seen [`concept`](https://leanprover-community.github.io/mathlib_docs/order/concept.html#concept)? This is a generalization of Dedekind cuts. Also I think your pointwise lemmas are all abstracted away in #13669 (by showing that `Sup` preserves addition,...

#3292 will allow us to how that `cut Q \~- R`, but we still need to build that `cut Q` is archimedean linear field. Am I missing something?