Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-28 23:50 77ba0c41

View on Github →

chore(logic): allow Sort* args in 2 lemmas (#10517)

Estimated changes

Modified src/logic/basic.lean

modified theorem congr_arg2

Modified src/logic/embedding.lean

modified theorem function.embedding.apply_eq_iff_eq