!4#5199: timeout problem in birthday problem

Stream: mathlib4

[Moritz Firsching]

In !4#5199, Wiedijk100Theorems.BirthdayProblem, I get a timeout, even with setting maxHeartbeats to 0.
Also maxRecDepth needed to be bumped.
I wonder if this is a regression or I'm just overlooking some simple fix.

[Eric Rodriguez]

having a look at this (it is my code so I feel a bit guilty!) it seems to be the big numbers causing issues

[Eric Rodriguez]

I thought this was meant to be fine because we were using GMP?

[Eric Rodriguez]

I pushed some working version, I think specifically the issue is big numbers coerced to ennreal

[Eric Rodriguez]

I do technically need this result: theorem _root_.ENNReal.mul_div (a b c : ℝ≥0∞) : a * (b / c) = (a * b) / c := sorry

[Eric Rodriguez]

I assume this is true but it may not be

[Eric Rodriguez]

also I had to extract have : ∀ a b : ℕ, 2 * a < b → 2 * (a : ℝ≥0∞) < b := fun _ _ h => by norm_cast; otherwise norm_cast goes haywire and tries to solve stuff it shouldn't be solving

[Eric Rodriguez]

also some simp_rws are painfully slow

[Eric Rodriguez]

this file is now compiling but I do think some of the issues are worth looking into

[Kevin Buzzard]

In my experience you only get people looking at timeouts/slowdowns if you demonstrate them with a #mwe that works on master.

[Jeremy Tan]

Eric Rodriguez said:

this file is now compiling but I do think some of the issues are worth looking into

There is no timeout. I got the original proof to work just by adding some newlines brackets

[Jeremy Tan]

It is now ready for review