-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
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
⊢ 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))))
have 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)
Tactic: ext ai ax bi bx ci cx : 6