priority 900

Stream: mathlib4

[Kevin Buzzard]

docs4#CategoryTheory.IsIso.comp_isIso has a lower than default priority because of possible loops. The comment and priority change have just been copied directly from mathlib3. I changed the priority back to default and nothing broke. Is there an argument for deleting the lowered priority? (PS the link to source in docs4 is still sending customers to example.com)

[Eric Wieser]

I think probably best to leave priority cleanups till after the port is done