search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.35k stars 298 forks source link

`continuity` tactic is not as capable as in mathlib3 #5030

Open semorrison opened 1 year ago

semorrison commented 1 year ago

Please link to this issue from porting notes.

semorrison commented 1 year ago

This link searches for references to this issue in the source code.

dwrensha commented 8 months ago

8312 brought us closer to parity with mathlib3 continuity.

Now continuity succeeds here: https://github.com/leanprover-community/mathlib4/blob/8e572f2640fb47dc1c0906a1df4af69ea504daa8/Mathlib/Analysis/ODE/PicardLindelof.lean#L305-L308 but unfortunately it also adds 800 milliseconds to elaboration time for that proof.

Similarly, now continuity succeeds here: https://github.com/leanprover-community/mathlib4/blob/8e572f2640fb47dc1c0906a1df4af69ea504daa8/Mathlib/Analysis/Calculus/Taylor.lean#L272 but it adds 90 milliseconds to elaboration time.

grunweg commented 2 months ago

13993 and #13994 will fix these issue (by changing these sites to use fun_prop instead, which is also much faster).