need help removing an erw

Stream: Infinity-Cosmos

[Emily Riehl]

PR #31101 is stuck (in part) because I'm unable to fulfill a request to remove an erw. See some discussion here:
#new members > how do I get rid of an erw? @ 💬

[Emily Riehl]

The erw appears on a hypothesis h.

Emily Riehl said:

I think I understand the confusion. Above I have
instance : Category (TransportEnrichment F C) := inferInstanceAs (Category C).

My hypothesis h refers to some structure borne by the type C. My goal involves morphisms in the category structure on the type TransportEnrichment F C.

So this is probably why rw [h] fails even though it looks like it should succeed. But I don't know how to fix it.

[Emily Riehl]

@Jakob von Raumer this has to do with your transport enrichment for enriched ordinary categories.

[Emily Riehl]

Also the build currently fails for some reason I don't understand, possibly related to the Mathlib.lean file? If someone has any clue how to fix that, it would be appreciated.

[Eric Wieser]

I've left a comment on fixing the build, the error was

Error: error: Mathlib.lean:1:0: cannot import non`-module` Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory from `module`