Debugging what simp does

Stream: new members

[Jakob Scholbach]

How can I see what simp is doing? Concretely, I have the following script, which works, but I want to avoid the begin / end and also the simp.

import category_theory.category
import category_theory.arrow

namespace category_theory

universes v₁ u₁
variables {C : Type u₁} [category.{v₁} C]

variables {A B X : C}

lemma square_of_comp_top_bottom (f : A ⟶ B) (g : B ⟶ X) : arrow.mk (f ≫ g) ⟶ arrow.mk g :=
begin
  have : f ≫ (arrow.mk g).hom = (arrow.mk (f ≫ g)).hom ≫ 𝟙 X :=
  begin
    simp,
    obviously,
  end,
  exact arrow.hom_mk this,
end

end category_theory

[Yakov Pechersky]

squeeze_simp and then replace with the proposed output

[Yakov Pechersky]

And should that be a def since the hom is data?

[Jakob Scholbach]

Ah, yes, it should be a def.

[Yakov Pechersky]

In this case, you're using tactics to make data. The tactics are very straightforward, so it's fine here, but the idiomatic way might be:

def square_of_comp_top_bottom' (f : A ⟶ B) (g : B ⟶ X) : arrow.mk (f ≫ g) ⟶ arrow.mk g :=
arrow.hom_mk (show f ≫ (arrow.mk g).hom = (arrow.mk (f ≫ g)).hom ≫ 𝟙 X, by { simp, obviously })

[Jakob Scholbach]

OK, thanks, will do that!

[Yakov Pechersky]

You also might prefer:

def square_of_comp_top_bottom'' (f : A ⟶ B) (g : B ⟶ X) : arrow.mk (f ≫ g) ⟶ arrow.mk g :=
arrow.hom_mk' (show f ≫ g = (f ≫ g) ≫ 𝟙 X, by simp)

[Yakov Pechersky]

because arrow.hom_mk' is specifically about making homs of the form arrow.mk f ⟶ arrow.mk g

[Yakov Pechersky]

Fully explicit (no need to, just for interest):

def square_of_comp_top_bottom'' (f : A ⟶ B) (g : B ⟶ X) : arrow.mk (f ≫ g) ⟶ arrow.mk g :=
arrow.hom_mk' (category.comp_id _).symm