mathlib
15c6eee7 - feat(logic/basic): Better congruence lemmas for `or`, `or_or_or_comm` (#12004)

Commit
3 years ago
feat(logic/basic): Better congruence lemmas for `or`, `or_or_or_comm` (#12004) Prove `or_congr_left` and `or_congr_right` and rename the existing `or_congr_left`/`or_congr_right` to `or_congr_left'`/`or_congr_right'` to match the `and` lemmas. Also prove `or_rotate`, `or.rotate`, `or_or_or_comm` based on `and` again. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading