-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (coeff
        (↑((l :
                (a :
                    (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2)) →
                  ↥(reesAlgebra I))
              (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
                ((single R n' : (a : M) → PolynomialModule R M) m) ⋯)) :
          R[X])
        (n + 1 - n'))
      m ∈
    I • F.N n
⊢ Membership.mem (α := M) (I • F.N n)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(reesAlgebra I)) (β := PolynomialModule R M)
            ((l :
                  (a :
                      (↑(⋃ (i : ℕ),
                            ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                        Type u_2)) →
                    ↥(reesAlgebra I))
                (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)
                  ((single R n' : (a : M) → PolynomialModule R M) m) ⋯) :
              ↥(reesAlgebra I))
            ((single R n' : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          (a : ℕ) → M)
        (n + 1) :
      M)

Tactic:
rw [Subalgebra.smul_def, smul_single_apply, if_pos (show n' ≤ n + 1 by lia)]

Premises used: if_pos, PolynomialModule.smul_single_apply, Subalgebra.smul_def