[Merged by Bors] - chore: @[simp] cancel_(right|left)

[semorrison]

---

• depends on: [Merged by Bors] - chore: remove reducible from Function.Surjective #6297

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: remove reducible from Function.Surjective #6297
  By Dependent Issues (🤖). Happy coding!

[semorrison]

!bench

[leanprover-bot]

Here are the benchmark results for commit d63c234.
There were significant changes against commit 68a37cd:

  Benchmark                                                           Metric         Change
  =========================================================================================
- ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions     5.9%

[semorrison]

One file got slower, but overall wall-clock is identical (epsilon faster), so I propose not worrying.

[kbuzzard]

I don't understand: how will the simplifier find these injectivity/surjectivity assumptions?

[jcommelin]

What is the motivation for this PR? Are you planning to golf some proofs in mathlib? Or some others?

[semorrison]

This was motivated by @jakelev and I working on our transport tactic, where we often have Injective or Surjective in the context and would like simp_all to just close obvious goals. Adding lemmas like this are very helpful for this.

So, no, not planning on golfing specific goals, we just wanted simp_all to be more powerful when there was already an Injective hypothesis available.

Not sure I'm going to have much opportunity to work on transport in the near future, so this isn't urgent.

[ocfnash]

I don't understand: how will the simplifier find these injectivity/surjectivity assumptions?

These can be triggered if simp figures out the injectivity hypothesis (say) some other way. For example if we added simp to RingHom.injective (and I'd argue we should) then the changes here should ensure that RingHom.cancel_left fires when the source is a division ring.

Mostly though the huge amount of repetition in the library that this PR highlights makes me wonder if cancel_left and cancel_right could be folder into the FunLike API.

[semorrison]

I don't understand: how will the simplifier find these injectivity/surjectivity assumptions?

@kbuzzard, e.g. aesop will use simp_all, so injectivity hypotheses in the local context are useful.

If you have an injectivity hypotheses h, it's also nice to just be able to write simp [h], without having to go find the names of the lemmas that use h.

[sgouezel]

Let's get this in. Thanks!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style