[Merged by Bors] - chore(data/sum): Add trivial simp lemmas

[eric-wieser]

---

Discussed here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/sum.2Eelim.20%28f.20.E2.88.98.20sum.2Einl%29.20%28f.20.E2.88.98.20sum.2Einr%29.20.3D.20f/near/217891929

@rwbarton points out that sum.elim_comp_inl_inr is shorter as ext (_|_); refl, but that's hard to use as a subexpression.

[fpvandoorn]

Given the objections on Zulip, the @[simp] attributes should probably be removed (except for elim_inl_inr). Other than that LGTM

[gebner]

This would also be fine as a simp lemma, but I'm not sure if we actually want this to always simplify to the right-hand side.

[eric-wieser]

Yeah, I left this one out because the decision of which way to simplify felt subjective.

[eric-wieser]

@gebner, do you agree with @fpvandoorn that only elim_inl_inr is safe to mark simp?

[gebner]

Yes. The only one I'm a bit antsy about is elim_comp_inl_inr but on closer inspection I don't think it would cause any problems.

[gebner]

bors r+

[eric-wieser]

Wait, now I'm confused. @fpvandoorn is asking me to remove the simp from everything but elim_inl_inr. Did you mean to type bors d+, or did you conclude these were all safe after all?

[gebner]

Ah, missed that comment.

bors r-
bors d=fpvandoorn

[bors]

✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Canceled.

[gebner]

I think all of them are safe tbh.

[fpvandoorn]

My comment was based on Gabriel's remark that the simp lemmas could be dangerous (and their limited use). If Gabriel is happy with them, so am I.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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