[Merged by Bors] - feat(logic/basic, logic/function/basic): make cast the simp-normal form of eq.mp and eq.mpr, add lemmas

[eric-wieser]

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.

---

[eric-wieser]

The failure is a bit odd; it's on this line:

mathlib/src/category_theory/filtered.lean

Line 230 in 0ded4eb

exact ⟨j, rfl, j', g, (by simp)⟩,

And it gets stuck at the goal

⊢ _ = _ ∧ _ = _

[gebner]

Should the simp lemmas be restricted to Type*? For Prop, they're completely trivial.

Another option is to give them a lower priority, so that eq_self_iff_true can trigger first.

[gebner]

The failure is a bit odd; it's on this line:

by simp is really overkill here. heq.rfl also works.

[gebner]

Another idea here would be to make cast the simp-normal form. That is, add lemmas eq.mp h x = cast h x etc.

[eric-wieser]

Good point about the lemmas being trivial for Prop. The simp normal form is a good idea too, but I have no idea what file that would go in. Should it go in core lean?

[gebner]

The simp normal form is a good idea too, but I have no idea what file that would go in. Should it go in core lean?

There is no reason to put it in core. I would put them into logic/basic or logic/function/basic.

[eric-wieser]

Should I just remove these, now that mp and mpr are rewritten into cast by simp?

[semorrison]

I wouldn't remove them. One can't be sure that simp will be able to reach every eq.mp.

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests