-- 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 :
  { 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) }
a :
  ∀ (xi : ι) (xv : A xi),
    Eq.{u_3 + 1} (α := 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)) ⋯)
                  ((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))
                    f)) :
              {i : ι} → A i →+ R) :
            (a : A xi) → R)
          xv :
        R)
      (((↑f : {i : ι} → A i →+ R) : (a : A xi) → R) xv : 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)) ⋯)
      ((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))
        f) =
    f

Tactic:
ext xi xv