Chaining Extensionality Lemmas in Lean’s Mathlib

In its most basic form, Lean’s or “extensionality” tactic reduces equalities of functions into equality at every evaluation , and equalities of sets into equivalence of membership in each set . The tactic is extensible; new scenarios can be enabled by adding an attribute to a theorem, for instance to add support for finite sets analogous to the support for sets. Where the tactic can provide particular value is when working with equalities of morphisms; for instance, to show that two linear maps from the tensor product of two modules agrees, it suffices to show that the two maps agree on the pure tensors. Using tensor products as the main example, this paper explores a well-established pattern in mathlib (championed largely by the author) that declares these extensions in a way that allows “chaining”; by preferring to state the assumption in terms of an equality of “partially-applied” morphisms, quantifying over elements only as a last result. Inevitably, the design of these tools shapes the way in which they are used; this paper concludes by noting how the tactic encourages expressing statements in a point-free manner, which at times impedes clarity.