Commit 2022-11-24 02:24 2d5a70de

View on Github →

feat(Data/Sum/Basic): sync with mathlib3 (#702)

  • Mathlib4 version of leanprover-community/mathlib#17059.
  • Drop simp attributes on Sum.getLeft etc. These attrs make Lean4 simplify getLeft x to a match expression, not only getLeft (inl x) to some x.

Estimated changes

added theorem Sum.Not_isLeft
added theorem Sum.Not_isRight
added theorem Sum.getLeft_inl
added theorem Sum.getLeft_inr
added theorem Sum.getLeft_map
added theorem Sum.getLeft_swap
added theorem Sum.getRight_inl
added theorem Sum.getRight_inr
added theorem Sum.getRight_map
added theorem Sum.getRight_swap
added theorem Sum.isLeft_eq_false
added theorem Sum.isLeft_iff
added theorem Sum.isLeft_inl
added theorem Sum.isLeft_inr
added theorem Sum.isLeft_map
added theorem Sum.isLeft_swap
added theorem Sum.isRight_eq_false
added theorem Sum.isRight_iff
added theorem Sum.isRight_inl
added theorem Sum.isRight_inr
added theorem Sum.isRight_map
added theorem Sum.isRight_swap
added theorem Sum.not_isLeft
added theorem Sum.not_isRight