# 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`.