Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 19:16 15c6eee7

View on Github →

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.

Estimated changes

added theorem Exists₂.imp
modified theorem and.rotate
added theorem and_rotate
added theorem forall₂_imp
added theorem or.rotate
added theorem or_congr_left'
modified theorem or_congr_left
added theorem or_congr_right'
modified theorem or_congr_right
added theorem or_or_or_comm
added theorem or_rotate