∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (N : ℕ → Submodule R M) (mono : ∀ (i : ℕ), N (i + 1) ≤ N i) (smul_le : ∀ (i : ℕ), I • N i ≤ N (i + 1))
  (N_1 : ℕ → Submodule R M) (mono_1 : ∀ (i : ℕ), N_1 (i + 1) ≤ N_1 i) (smul_le_1 : ∀ (i : ℕ), I • N_1 i ≤ N_1 (i + 1)),
  ({ N := N, mono := mono, smul_le := smul_le } = { N := N_1, mono := mono_1, smul_le := smul_le_1 }) = (N = N_1)