-- 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]
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
⊢ 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))
have 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))
Tactic: subst this
Cleared hypotheses: i, ih, hmby, h1, h2, this