-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
refine_1 :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) 0),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) 0 hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            0 hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
⊢ ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x),
    Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (↑(Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) x hx) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
              ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
            x hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
have refine_2 : ∀ (a : M) (b : R) (f_1 : M →₀ R),
  a ∉ f_1.support →
    b ≠ 0 →
      (∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) f_1),
          Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
            ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
                (↑(Subtype.mk (p := fun (x : R[M]) ↦
                      Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) f_1 hx) :
                  R[M]) :
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
            (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
                    ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
                  (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
                (Subtype.mk (p := fun (x : R[M]) ↦
                  Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) f_1 hx) :
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))) →
        ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single a b + f_1)),
          Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
            ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
                (↑(Subtype.mk (p := fun (x : R[M]) ↦
                      Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
                      (Finsupp.single a b + f_1) hx) :
                  R[M]) :
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
            (((DirectSum.of (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) i :
                    ↥(gradeBy R (⇑f : (a : M) → ι) i) →+ ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
                  (a : ↥(gradeBy R (⇑f : (a : M) → ι) i)) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
                (Subtype.mk (p := fun (x : R[M]) ↦
                  Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x) (Finsupp.single a b + f_1)
                  hx) :
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
Tactic: refine Finsupp.induction x ?_ ?_