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.