Lemma 7.2.4 already proved in Corollary 3.2.7

[louisGarde]

We should better prove it once in chapter 3.2 and refer to it in chapter 7.2.

[mikeshulman]

Hmm... separating it out as a new lemma in chapter 3 would require #613, which no one else seems to want. But I guess 7.2.4 could refer to the proof of 3.2.7.

[mikeshulman]

I propose that for the first edition we simply add a comment, #865. In the second edition we can clean it up a bit more.