speeding up category theory

Stream: maths

[Kevin Buzzard]

Every now and then I attempt to engage with the category theory library and I always manage get a bit further in than the time before. And then I usually run into something which frustrates me (e.g. I get muddled about universes) and moan here for a bit and then go and do something else.

So @Calle Sönne raised the question of proving that the equalizers of (f,g) and (g,f) are isomorphic. If I write down the map like this:

import category_theory.limits.shapes.equalizers

open category_theory
open category_theory.limits

universes v u

variables {C : Type u} [𝒞 : category.{v} C] [has_equalizers.{v} C]
include 𝒞

variables (A B : C) (f g : A ⟶ B)

set_option profiler true
def equalizer.symm.hom : equalizer g f ⟶ equalizer f g :=
equalizer.lift _ _ (equalizer.ι g f) (by tidy)
-- elaboration of equalizer.symm.hom took 794ms

then things are already slow. I changed tidy to simp and it's still slow. My impression is that in Isabelle you replace by tidy with sledgehammer and then look at the output and use that in your code instead. Is there a way of doing this here?
Isn't there some way of getting tidy to report tidy says...? I know I can put simp logging on but if I could just get something to cut and paste that would be great.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#tidy

[Kevin Buzzard]

boggle why do I have to look at this web page? I even read the Lean source for tidy. Shouldn't this be mentioned in the docstring?

[Patrick Massot]

Documentation can always be improved, but that one was not so hard to find...

[Kevin Buzzard]

If I hover over tidy I get tidy ?? tactic.tidy.cfg?

[Patrick Massot]

But you can PR a better docstring of course.

[Kevin Buzzard]

Documentation can always be improved, but that one was not so hard to find...

It's not so hard to find if you remember all the places where you're supposed to be looking to find this information. I tried the docstring, I tried the source code for the file hoping for a module docstring, I tried searching Zulip for tidy says, I then asked here.

[Kevin Buzzard]

I can't write this docstring. "Tidy does something. Try tidy? to see what it did."

[Kevin Buzzard]

oh wait, I can -- I can just copy from the tactic md file ;-)

[Kevin Buzzard]

Is it [ci skip] or [skip ci] in the commit message? Both have been used recently. Do both work?

[Kevin Buzzard]

#1788

[Patrick Massot]

I think both [ci skip] and [skip ci] work, although the first one is the legit one.