-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
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]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih :
  ∀ (hx : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) y),
    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) y 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)
            y hx) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
hmby : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) (Finsupp.single m b + y)
this_1 : Disjoint (Finsupp.support (Finsupp.single m b)) y.support
h1 : (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
h2 : (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) {i}
this : (f : (a : M) → ι) m = i
refine_2 :
  ∀
    (ih :
      ∀
        (hx :
          Membership.mem (γ := Submodule R R[M])
            (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) y),
        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.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι))
                      x)
                    y hx) :
                R[M]) :
            ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) m : ι) :
                  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) →+
                    ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
                (a : ↥(gradeBy R (⇑f : (a : M) → ι) ((f : (a : M) → ι) m))) →
                  ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
              (Subtype.mk (p := fun (x : R[M]) ↦
                Membership.mem (γ := Submodule R R[M])
                  (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
                y hx) :
            ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)))
    (hmby :
      Membership.mem (γ := Submodule R R[M])
        (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι))
        (Finsupp.single m b + y))
    (h1 :
      (↑(Finsupp.support (Finsupp.single m b)) : Set M) ⊆
        Set.preimage (β := ι) (⇑f : (a : M) → ι) (singleton (α := ι) ((f : (a : M) → ι) m : ι)))
    (h2 :
      (↑y.support : Set M) ⊆ Set.preimage (β := ι) (⇑f : (a : M) → ι) (singleton (α := ι) ((f : (a : M) → ι) m : ι))),
    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.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
                (Finsupp.single m b + y) hmby) :
            R[M]) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
      (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) m : ι) :
              ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) →+
                ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a : ↥(gradeBy R (⇑f : (a : M) → ι) ((f : (a : M) → ι) m))) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          (Subtype.mk (p := fun (x : R[M]) ↦
            Membership.mem (γ := Submodule R R[M])
              (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
            (Finsupp.single m b + y) hmby) :
        ⨁ (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))
        (↑(Subtype.mk (p := fun (x : R[M]) ↦ Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) x)
              (Finsupp.single m b + y) hmby) :
          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 m b + y) hmby) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
subst this