mathlib

879273e8 - feat(logic/basic, logic/function/basic): make `cast` the simp-normal form of `eq.mp` and `eq.mpr`, add lemmas (#6834)

feat(logic/basic, logic/function/basic): make `cast` the simp-normal form of `eq.mp` and `eq.mpr`, add lemmas (#6834) This adds the fact that `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` are bijective, as well as some simp lemmas that follow from their injectivity.