-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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)
⊢ (fun
          (a₁ :
            (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
              Type u_2))
          (b : ↥(reesAlgebra I)) ↦
        ((b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1) : M))
      (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) ⋯)
      ((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) ⋯)) ∈
    I • F.N n
have dsimp : 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) sorry) :
            ↥(reesAlgebra I))
          ((single R n' : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) :
    M)
Tactic: dsimp only [Subtype.coe_mk]