Chapter 3.5 done - example 3.5.9 slowdown

Stream: Analysis I

[Rado Kirov]

Finally done with chapter 3.5. I feel I am starting to grok subtypes and how to work with Classical.choice. Exercise 3.5.12 and 3.5.13 were quite challenging but fun.

Example 3.5.9 for whatever reason turned out really slow down Lean to the point that I had to type and wait ~10-20 sec for any feedback and extend heartbeats to get output. Luckily the solutions were short at the end.

I would be curious to know if someone else manages to avoid that slowdown by working with better theorems (my solutions are here https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_3_5.lean#L567-L721). Also if there is any tracing/debugging I can do to pin point the slowdown that would be helpful.

There are few _eval lemmas that I found lacking and can contribute back to the repo if folks agree they are generally useful - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_3_5.lean#L567-L721

[Terence Tao]

putting set_option trace.profiler true in at the start of a theorem gives you a trace in the infoview. If one continually clicks on the little triangles that report the most seconds used, you will eventually find the heartbeat culprit. Replacing simp with simp only via simp? may remove at least some of the slowdown, though simp isn't that heartbeat-intensive.

The fst and snd operations on X ×ˢ Y should come with some spec lemma which should make eval lemmas about them easier to use. The pairing map X → Y → X ×ˢ Y that is implicitly in curry should probably be made more explicit, with the eval lemmas being that this pairing map is basically inverted by fst and snd.

[Rado Kirov]

For the second part, I opened https://github.com/teorth/analysis/pull/229