Go back to the tag's page.
Tags: Added new tags
Fix two typos
Split out the steps in Lemma Tag 05U9 This produces a bunch of cases where we know the lemma is true, including the one case which is actually used later.