Commit 2019-07-02 04:29 57b57b38

feat(data/equiv/basic): improve arrow_congr, define conj (#1119)

• feat(data/equiv/basic): improve arrow_congr, define conj

• redefine equiv.arrow_congr without an enclosing match
• prove some trivial lemmas about equiv.arrow_congr
• define equiv.conj, and prove trivial lemmas about it

• chore(data/equiv/basic): add @[simp] Also split some long lines, and swap lhs with rhs in a few lemmas.
• Reorder, drop TODO