-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
H :
  ∀ (ai : ιA) (ax : A ai) (bi : ιA) (bx : A bi) (ci : ιB) (cx : M ci),
    Eq (α := ⨁ (i : ιB), M i)
      ((comp
              ((comp
                    ((comp
                          (comp
                            ((compHom :
                                (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
                                  ((⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) →+
                                    (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                              (smulAddMonoidHom A M))
                            (mulHom A))
                          (of A ai) :
                        (a : A ai) → (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                      ax)
                    (of A bi) :
                  (a : A bi) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                bx)
              (of M ci) :
            (a : M ci) → ⨁ (i : ιB), M i)
          cx :
        ⨁ (i : ιB), M i)
      ((comp
              ((comp
                    ((comp
                          (AddMonoidHom.flip
                            ((((compHom :
                                      (a :
                                          ((⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                                            (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
                                        ((⨁ (i : ιA), A i) →+
                                            (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                                          (⨁ (i : ιA), A i) →+
                                            (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                                    flipHom :
                                  ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                                    (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
                                (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
                                  (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                              (comp (N := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                                ((compHom :
                                    (a : (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
                                      ((⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →+
                                        (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i)
                                  (AddMonoidHom.flip (smulAddMonoidHom A M)))
                                (smulAddMonoidHom A M))))
                          (of A ai) :
                        (a : A ai) → (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                      ax)
                    (of A bi) :
                  (a : A bi) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                bx)
              (of M ci) :
            (a : M ci) → ⨁ (i : ιB), M i)
          cx :
        ⨁ (i : ιB), M i)
⊢ Eq (α := (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
    (comp
      ((compHom :
          (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
            ((⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
        (smulAddMonoidHom A M))
      (mulHom A))
    (AddMonoidHom.flip
      ((((compHom :
                (a :
                    ((⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                      (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
                  ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                    (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              flipHom :
            ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
              (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
            (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
        (comp (N := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
          ((compHom :
              (a : (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
                ((⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i)
            (AddMonoidHom.flip (smulAddMonoidHom A M)))
          (smulAddMonoidHom A M))))

Tactic:
ext ai ax bi bx ci cx : 6