basic): Add trivial simp lemma (#5100)

Commit

5 years ago

chore(data/equiv/basic): Add trivial simp lemma (#5100) With this in place, `⇑1 ∘ f` simplifies to `⇑f`

Author

eric-wieser

Parents