-- 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 : ↥(gradeBy R (⇑f : (a : M) → ι) i)
obtain obtain₁ :
  ∀ (x : R[M]) (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))
refine_1 :
  ∀ (x : R[M]) (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))
⊢ Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (↑x : 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))
        x :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
have refine_2 : ∀ (x : R[M]) (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: classical
  obtain ⟨x, hx⟩ := x
  revert hx
  refine Finsupp.induction x ?_ ?_
  · intro hx
    symm
    exact map_zero _
  · intro m b y hmy hb ih hmby
    have : Disjoint (Finsupp.single m b).support y.support := by
      simpa only [Finsupp.support_single _ hb, Finset.disjoint_singleton_left]
    rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff]
      at hmby
    obtain ⟨h1, h2⟩ := hmby
    have : f m = i := by
      rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
        at h1
    subst this
    simp only [map_add, decomposeAux_single f m]
    let ih' := ih h2
    dsimp at ih'
    rw [ih', ← map_add]
    apply DirectSum.of_eq_of_gradedMonoid_eq
    congr 2
Cleared hypotheses: x