to_jordan_decomposition_smul

Stream: general

[Scott Morrison]

Would anyone be interested in diagnosing the mysteriously-rather-slow docs#measure_theory.signed_measure.to_jordan_decomposition_smul?

[Eric Wieser]

Does squeezing the simp help?

[Stuart Presnell]

Changing the simp line to:

simp only [to_signed_measure_smul, to_signed_measure_to_jordan_decomposition]

closes the goal quickly. That doesn't explain why simp takes so long to find an answer, though.