Dot notation

Say you have a type, like subgroup G, and a term of that type, like H : subgroup G. Say you have a function in the subgroup namespace which takes as input a term of type subgroup G, for example subgroup.inv_mem, which has as an explicit input a term H : subgroup G and spits out a proof that x ∈ H → x⁻¹ ∈ H. Then instead of writing subgroup.inv_mem H : x ∈ H → x⁻¹ ∈ H you can just write H.inv_mem : x ∈ H → x⁻¹ ∈ H.

In general the rule is that if you have a term H : foo ... of type foo or foo A B or whatever, and then you have a function called foo.bar which has an explicit (i.e., round brackets) input of type foo ..., then instead of foo.bar H you can just write H.bar. This is why it’s a good idea to define theorems about foo``s in the ``foo namespace.

This sort of trick can be used all over the place; it’s surprisingly powerful. For example Lean has a proof eq.symm : x = y → y = x. If you have a term h : a = b then, remembering that = is just notation for eq so that h really has type eq a b, you can write h.symm : b = a as shorthand for eq.symm h.