-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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
⊢ 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)
have 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)) sorry sorry : (⨁ (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)) sorry)
                  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)
Tactic: refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))