-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
a :
  ∀ (xi : ι) (xv : A xi),
    Eq.{u_3 + 1} (α := R)
      ((AddMonoidHom.comp
              ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R))
                ((fun
                      (f :
                        { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
                          Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                            ∀ {i j : ι} (ai : A i) (aj : A j),
                              (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                                HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R)
                                  ((f : (a : A j) → R) aj : R) }) ↦
                    (toSemiring (A := A) (fun (x : ι) ↦ (↑f : {i : ι} → A i →+ R)) ⋯ ⋯ : (⨁ (i : ι), A i) →+* R))
                  ((fun (F : (⨁ (i : ι), A i) →+* R) ↦
                      Subtype.mk (p := fun (f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R) ↦
                        Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                          ∀ {i j : ι} (ai : A i) (aj : A j),
                            (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                              HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R))
                        (fun {i : ι} ↦ AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i)) ⋯)
                    F)))
              (of A xi) :
            (a : A xi) → R)
          xv :
        R)
      ((AddMonoidHom.comp
              ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)
              (of A xi) :
            (a : A xi) → R)
          xv :
        R)
⊢ Eq (α := (⨁ (i : ι), A i) →+ R)
    ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R))
      ((fun
            (f :
              { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
                Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                  ∀ {i j : ι} (ai : A i) (aj : A j),
                    (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                      HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R) }) ↦
          (toSemiring (A := A) (fun (x : ι) ↦ (↑f : {i : ι} → A i →+ R)) ⋯ ⋯ : (⨁ (i : ι), A i) →+* R))
        ((fun (F : (⨁ (i : ι), A i) →+* R) ↦
            Subtype.mk (p := fun (f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R) ↦
              Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                ∀ {i j : ι} (ai : A i) (aj : A j),
                  (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                    HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R))
              (fun {i : ι} ↦ AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i)) ⋯)
          F)))
    ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)

Tactic:
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'