[Merged by Bors] - chore(data/equiv/basic): arrow_congr preserves properties of binary operators

[eric-wieser]

---

[urkud]

I added function.semiconj₂ versions of some proofs and moved the new section below conj. BTW, you can write e.conj instead of e.arrow_congr e but you have to use the same form everywhere if you want lean to find instances.

[eric-wieser]

My hope was that lean would be able to unfold conj to find the instances in this PR. Perhaps that's not how that works.

Would it make sense to add a e.conj₂ as a shorthand for e.arrow_congr (e.arrow_congr e)? (in a later PR?)

[urkud]

AFAIK, lean will be able to unfold conj if you make it reducible. BWT, what is your use case? If you want to transfer some standard algebraic structure (monoid etc), then we already have defs/lemmas for that.

[eric-wieser]

BWT, what is your use case?

I needed two of these instances to call finset.fold, and figured I'd add the other easy ones. In turn, I wanted that to build a non-cheating proof for the to_dual PR.

[jcommelin]

LGTM, @urkud any comments?

[urkud]

@jcommelin LGTM
I didn't merge it because I golfed some proofs.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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