The design does not follow the existing design of the heterogenous version, GradedMonoid.GSmul

I really need three different graded objects (not just 1 or 2), and for my main purposes (composition of cochains in the Hom complex between two cochain complexes K and L), using the current design would only make things more complicated rather than simplifying them. I shall just define my types Cochain K L n for all n : ℤ and a composition Cochain.comp following the design outlined in this PR (without the typeclass and the notation), as I had done it initially.

using the current design would only make things more complicated rather than simplifying them

To be clear, my claim is mostly "we should not have both designs in mathlib simultaneously", and not necessarily "the current design is better than this one". If you feel the currently design makes things hard, then presumably it makes things hard for the existing algebraic uses too.

The current design seems to be more focused on the situation where we have a ring, which happens to have an internal decomposition into homogeneous components. For the applications I am considering (certain types of cochains, Ext-groups), it does not seem to me that the current API would enable me to conveniently consider the multiplication as a map X a → X b → X c whenever a + b = c (e.g. 0 + 0 = 0, 1 + (n-1) = n, n + 0 = n, etc.), which is very critical for the applications I am considering. (In the current API, we have a few cases like 0 + 0 = 0 and 0 + n = n, but I want more!)

Indeed, when the degrees are related to categorical constructions, replacing a + b by any c such that a + b = c has already proven useful. During the port, refactoring the API of shifts on categories (see shiftFunctorAdd' in CategoryTheory.Shift.Basic) enabled me to simplify proofs about the rotation of triangles in triangulated categories. I have been able to develop derived categories using this idea multiple times. More recently, using similar principles, I unblocked the proof of the pentagon axiom for the monoidal structure on graded objects (see #6379).

Would you consider changing the definition of GMul (and al.) so that it would contain a field like {i j k} (h : i + j = k) : A i → A j → A k rather than {i j} : A i → A j → A (i + j). It would be suitable for what I would like to do, and on the other hand, if they want to construct a term of type GMul, the user may still do rintro i j _ rfl x y if they wish to do so!

The current design seems to be more focused on the situation where we have a ring, which happens to have an internal decomposition into homogeneous components.

This was indeed the original motivation, but it also works for graded monoids, taking the approach of bundling the index into a sigma type to avoid having to deal with dependent types.

More recently, using similar principles, I unblocked the proof of the pentagon axiom for the monoidal structure on graded objects (see #6379).

Do you have a specific hunk of this PR in mind that I could compare to?

It would be suitable for what I would like to do, and on the other hand, if they want to construct a term of type GMul, the user may still do rintro i j _ rfl x y if they wish to do so!

Note that I could make the same claim in the other direction, by defining your gmul h x y as equiv.cast (congr_arg X h) (my_gmul a b)! I think this is a tradeoff between producers of your API (instance) and consumers using the lemmas, and it's not clear to me which approach is better for who.

More recently, using similar principles, I unblocked the proof of the pentagon axiom for the monoidal structure on graded objects (see #6379).

Do you have a specific hunk of this PR in mind that I could compare to?

There is not much to compare because it would be a comparison between a proof of https://github.com/leanprover-community/mathlib4/pull/6379/files#diff-bdcce763b9b5b027315a99b7d248b577247fb39d8c4eca5106845cce8ea4bdafR615 and a sorry. The proof builds on definitions/lemmas like https://github.com/leanprover-community/mathlib4/pull/6379/files#diff-bdcce763b9b5b027315a99b7d248b577247fb39d8c4eca5106845cce8ea4bdafR306-R309 (the key point is that the assumption p₁ + p₂ + p₃ = n does not need to be a defeq).

Note that I could make the same claim in the other direction, by defining your gmul h x y as equiv.cast (congr_arg X h) (my_gmul a b)! I think this is a tradeoff between producers of your API (instance) and consumers using the lemmas, and it's not clear to me which approach is better for who.

Of course, we can use equiv.cast to do what I suggest, but this is not very satisfactory. It is like having to deal with annoying eqToHom in category theory: this is precisely what I made disappear (or dissolve in the API) in my refactor of shifts in category theory and in the proof of a pentagonal identity mentionned above.

The suggestion I made would not be detrimental to the current API, and at the same time it would enable other uses. I certainly do not want to go to the sigma type: I want to be able to state equalities of cochains (e.g. associativity of the composition) as an equality of two cochains of a certain degree, certainly not just as an equality in a larger type.

In #6701 I define the cochains I have been mentioning above and their composition, which would be an example of "graded heterogeneous multiplication".

Using HMul for generalized compositions is a nice idea, though I think if we're going to do so we should try it out in linear algebra first. If that works, then I agree that probably a heterogenous version of GradedMonoid.GMul is reasonable; but we still should try and align the designs.