[Merged by Bors] - chore(CategoryTheory/Comma/Arrow): restore use of inferInstanceAs

[JovanGerb]

This PR fixes the category instance on Arrow to be less leaky. This is a fix after the refactor in #37764.

---

[github-actions]

PR summary 044631201f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance : Quiver (Arrow T)

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 6b12b77 against 0446312 are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +17.0G (+0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.Tactic.FunProp.Decl//instructions: -293.6M (-4.72%)

[JovanGerb]

I think the performance impact is neutral.

[dagurtomas]

I'm sure this is the correct thing to do, but can you explain a bit what the issue was? And why doesn't

instance : Category (Arrow T) where
  Hom := Arrow.Hom
  __ := inferInstanceAs <| Category (Comma (𝟭 T) (𝟭 T))

work?

[JovanGerb]

The issue is in the data fields id and comp. In the old version, these had types corresponding to Comma (𝟭 T) (𝟭 T). inferInstanceAs packages the data so that the definition doesn't leak through.

The option you suggested doesn't compile. It is possible to write

instance : Category (Arrow T) where
  Hom := Arrow.Hom
  __ : Category (Arrow T) := inferInstanceAs <| Category (Comma (𝟭 T) (𝟭 T))

And this does give the right defeq. But the generated term is a lot more unnecessarily complicated. #print instCategoryArrow gives

  let __spread.0 :=
    { Hom := instCategoryArrow._aux_1, id := instCategoryArrow._aux_3, comp := @instCategoryArrow._aux_5 T inst,
      id_comp := ⋯, comp_id := ⋯, assoc := ⋯ };
  { Hom := Arrow.Hom, id := 𝟙, comp := @CategoryStruct.comp (Arrow T) __spread.0.toCategoryStruct, id_comp := ⋯,
    comp_id := ⋯, assoc := ⋯ }

[robin-carlier]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[joelriou]

I would trust your judgement here!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build