Commit 2021-08-26 03:51 7e781a8e

chore(*): Fix syntactic tautologies (#8811) Fix a few lemmas that were accidentally tautological in the sense that they were equations with syntactically equal LHS and RHS. A linter will be added in a second PR, for now we just fix the found issues. It would be great if a category expert like @semorrison would check the category ones, as its unclear to me which direction they are meant to go. As pointed out by @PatrickMassot on Zulip https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/syntactic.20tautology.20linter/near/250267477. Thanks to @eric-wieser for helping figure out the corrected versions.