Might be handy to state this with Bijective as well (Involutive is unfortunately not type-correct), or bundle it as flipEquiv

IIUC you're suggesting a lemma stating Bijective (RootPairing.flip (ι := ι) (R := R) (M := M) (N := N)) or similar?

I think it's not so likely this will be useful so I'd rather wait and see. No strong feelings though: I can add it if you think I really should.

Similar remarks for my understanding of the other suggestion:

variable (ι R M N) in
def flipEquiv : RootPairing ι R N M ≃ RootPairing ι R M N where
  toFun P := P.flip
  invFun P := P.flip
  left_inv _ := rfl
  right_inv _ := rfl

The application I'm thinking of is one where you'd prefer to argue by flipping all the root pairings, either via Injective or via Surjective.forall. Bijectivity follows trivially from Equiv.bijective, but I think it's still worth stating explicitly to get in the simp normal form.

Maybe this type of argument never comes up, but it's always handy if the construction is already in the library when a future user needs it!

I find it very hard to imagine a situation like the one you describe arising but as a compromise, I've added flipEquiv for both RootPairing and RootSystem.

Does the informal literature include definitions for non-reduced or infinite root systems?
(I've only ever studied the happy path.)

Could you please add some explicit refs to the literature?

I really only know the finite story, and I think the infinite story is tricky, not least because IIUC there isn't an axiomatic account of infinite root systems: people always seem to start with a basis of simple roots and a (generalised) Cartan matrix. I do recall reading some old paper of Kac in which he observes that linear independence is the wrong condition (after Scott pointed this out to me) but if I am to supply a reference for the infinite case here I'd rather use one suggested by @ScottCarnahan

As to the finite case, I am indeed diverging from the informal literature. E.g., both Bourbaki and Serre ("Complex Semisimple Lie Algebras") define the concept of base for non-reduced systems (using different definitions). However I really think what I'm defining here is the "right" object. For a non-reduced (crystallographic) root system (in Bourbaki / Serre) if $\alpha$ belongs to a base and you want the corresponding coroot to form a base of the coroots then it is either $\check{\alpha}$ if $2\alpha$ is not a root or else it is $\check{\alpha}/2$. Also it is only for reduced systems that you get the simply transitive action of the Weyl group on bases (and of course the Weyl group is unchanged if you pass from a non-reduced root system to the reduced system of indivisible roots).

I certainly will understand if you think we shouldn't diverge here but I claim that it is the right call as long as we highlight it sufficiently clearly in the doc string.

Thanks for these clarifications. I think they should be preserved in this file.
Maybe the discussion is too long for the docstring. But please add them (at least the finite case) to the module docstring, and add a pointer to this discussion from the docstring of RootSystem.Base.

I think especially in the finite case, it is important that we justify the divergence from the literature. After all, Bourbaki and Serre are mostly considered "ground truth".
But if Scott has remarks about the infinite case that should also be added to the discussion, I would love to hear those as well. We can add those in a later PR.

I've added these remarks to the module doc string and added a pointer to that from the definition doc string (which I have also shortened).