I think this is a very nice project and a very nice approach for a foundational topic such as analysis. A couple immediate worries: 1. Core analysis results i

I think this is a very nice project and a very nice approach for a foundational topic such as analysis. A couple immediate worries: 1. Core analysis results in Mathlib work with limits in a general, unified way using the notion of filters. There are nevertheless some ad-hoc specializations of these results to their epsilon-delta form. I presume that Tao's Analysis uses a more traditional epsilon-delta approach. 2. Mathlib moves fast and breaks things. Things get renamed and refactored all the time. Downstream repos needs continual maintenance.