mathlib
8cd5f0ee - chore(category_theory/isomorphisms): Adjust priority for is_iso.comp_is_iso (#10276)

Commit
4 years ago
chore(category_theory/isomorphisms): Adjust priority for is_iso.comp_is_iso (#10276) [See Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/iso.20to.20is_iso.20for.20types/near/261122457) Given `f : X ≅ Y` with `X Y : Type u`, without this change, typeclass inference cannot deduce `is_iso f.hom` because `f.hom` is defeq to `(λ x, x) ≫ f.hom`, triggering a loop. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Author
Parents
Loading