-- 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 :
  { 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 (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
have 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)) sorry)
                ((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))
                  f)) :
            {i : ι} → A i →+ R) :
          (a : A xi) → R)
        xv :
      R)
    (((↑f : {i : ι} → A i →+ R) : (a : A xi) → R) xv : R)
Tactic: ext xi xv