intervalIntegral.integral_const_mul is not a good simp lemma

Stream: mathlib4

[Michael Stoll]

... because simp will change

∫ (t : ℝ) in a..b, r * f t = ∫ (t : ℝ) in a..b, r / g t

to

r * ∫ (t : ℝ) in a..b, f t = ∫ (t : ℝ) in a..b, r / g t

So to make it reasonable, a lemma that pulls out r from the RHS would be needed.
docs#intervalIntegral.integral_const_mul docs#intervalIntegral.integral_mul_const

But I would question the assumption that having the constant factor outside is necessarily the simpler form.

[Kevin Buzzard]

well we could always make div_eq_mul_inv a simp lemma ;-)

(context: back before the Lean 3 fork, sub_eq_add_neg was a simp lemma in core and it drove everyone nuts. It was one of the first things to be changed after the fork IIRC)

[Yaël Dillies]

I agree with you, Michael. The simp lemma should go the other way, because it's a distributivity lemma. See docs#Finset.mul_sum.

[Michael Stoll]

Whatever the reasonable direction is, it should be consistent between addition, sums, and integrals.

[Yaël Dillies]

Yes, so that's a :+1: from me to turn your integral lemma around.

[Michael Stoll]

It's not "my" lemma :smile:
I have enough rabbit holes to get myself lost in already, so I won't go down this one.