Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-13 21:36 71a3261c

View on Github →

feat(logic/basic): exists_eq simp lemmas without and.comm (#5694)

Estimated changes

Modified src/control/traversable/instances.lean

Modified src/data/buffer/parser/basic.lean

deleted theorem exists_eq_right_right'

deleted theorem exists_eq_right_right

Modified src/data/list/perm.lean

Modified src/logic/basic.lean

added theorem exists_eq_right_right'

added theorem exists_eq_right_right