Confused by "failed to synthesize type class instance" error

Stream: new members

[Sara Fish]

To practice writing definitions, I am trying to define what it means for an element $g$ of a group $G$ to generate $G$. I have the definition

def is_generator (G : Type) (g : G) [group G] :=
∀ h ∈ G, ∃ k ∈ ℕ, g^k = h

This gives the error

failed to synthesize type class instance for
G : Type,
g : G,
_inst_1 : group G,
h : G,
H : h ∈ G,
k : ?m_2
⊢ has_mem ?m_2 Type

What does this mean? How can I fix this definition?

[Dan Stanescu]

Use k : \N instead of k \in \N in your definition.

[Sara Fish]

Ah, thanks. So \in is for sets specifically and : is for when something is just any term of that type?

[Carl Friedrich Bolz-Tereick]

exactly (this also confuses me often)

[Kyle Miller]

I found it to be helpful to look carefully at the definitions for how set membership works. A term s of set X is nothing more than a function X → Prop, and for sets x ∈ s is defined to be s x. (See set.mem, which is attached to the ∈ notation through the has_mem instance on the next line).

So, a "set" in Lean is more like a subset of a given type, and it is given by an indicator function.

You can turn a set into a type using subtype, which is usually done either through an automatic coercion in certain places or by up arrow notation. As an example of an automatic coercion, you can write the binder x : s when s is a set. But then x is a slightly different thing, where x.val is the actual term in X and x.property is the proof that x ∈ s.

Maybe it's also worth knowing that when you write ∀ x ∈ s, ... it's equivalent to ∀ (x : X) (H : x ∈ s), ....

[Carl Friedrich Bolz-Tereick]

thanks for this detailed explanation!