# Commit 2019-07-02 04:29 57b57b38

View on Github →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