!4#4710 IntervalIntegral

Stream: mathlib4

[Johan Commelin]

The simp linter is quite upset about this PR. I don't know if we took a wrong turn somewhere...

[Yury G. Kudryashov]

This PR has a bunch of lemmas about integrals of, e.g., f (x + c). I understand that in nontrivial situations it may be hard for Lean to match a lemma like this. Should we drop these @[simp] attributes (for now)?

[Jireh Loreaux]

@Yury G. Kudryashov can you link to a discussion or explanation of why Lean will find these lemmas hard to match? Is it because we now use discrimination tree indexing or something?

[Yury G. Kudryashov]

I think, it's generally hard to match if x appears several times.

[Yury G. Kudryashov]

E.g., (x + 3) ^ 2 + sin (x + 3) but bigger.

[Yury G. Kudryashov]

But this is a guess.

[Johan Commelin]

@Yury G. Kudryashov Let's just drop @[simp] for now. But we might want to have an extra porting note at the top of the file or something...

[Yury G. Kudryashov]

Done. Waiting for CI