simplify type of term in goal

Stream: general

[Winston Yin]

My goal contains an expression like g ≫ f. If I hover over f and g in VSCode, I see that g : X ⟶ Y and f : Y ⟶ really_complicated_stuff. I know that really_complicated_stuff = simple_stuff. I even have a simp lemma for that. What I want to do is do a rewrite using a lemma g ≫ f = ..., which is stated for f : Y ⟶ simple_stuff. However, when I try that, Lean complains that it can't find g ≫ f in the goal, even when the pretty printer literally prints g ≫ f. What can I do?

If I do set f' := f with h, Lean even can't rw ←h because of type check difficulties. Please advise.

[Eric Wieser]

Can you make a #mwe?

[Johan Commelin]

Hmm, your example doesn't seem to typecheck. Do you want f : Y \hom simple_stuff? You are talking about f : simple_stuff halfway through your message.
I think it is hard to debug this without more details.

[Eric Wieser]

even when the pretty printer literally prints g ≫ f. What can I do?

You can use set_option pp.all true to check a little more thoroughly whether they're really the same

[Winston Yin]

Fixed typo in question

[Andrew Yang]

Though I do not have a #mwe as well, I can confirm this occurs on me from time to time, where I would like to dsimp on the type of the terms. And it is quite annoying to fix, usually resulting in some ugly change or erw.

[Andrew Yang]

(Hopefully the really_complicated_stuff = simple_stuff is defeq. It's evil to talk about equality of objects otherwise.)

[Winston Yin]

Yes they are defeq. The equality is a simp lemma proved with rfl. I managed to circumvent the problem by making f start out as Y ⟶ simple_stuff rather than Y ⟶ complicated_stuff