[Merged by Bors] - chore: mark CategoryTheory.Limits.pair as implicit_reducible - #42721

[Merged by Bors] - chore: mark CategoryTheory.Limits.pair as implicit_reducible#42721

JovanGerb wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

JovanGerb:Jovan-CategoryTheory.Limits.pairJovanGerb/mathlib4:Jovan-CategoryTheory.Limits.pairCopy head branch name to clipboard