# Zulip Chat Archive

## Stream: new members

### Topic: Confused by "failed to synthesize type class instance" error

#### Sara Fish (Jul 17 2020 at 19:04):

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 (Jul 17 2020 at 19:05):

Use `k : \N`

instead of `k \in \N`

in your definition.

#### Sara Fish (Jul 17 2020 at 19:07):

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

#### Carl Friedrich Bolz-Tereick (Jul 17 2020 at 19:10):

exactly (this also confuses me often)

#### Kyle Miller (Jul 17 2020 at 19:50):

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 (Jul 17 2020 at 19:59):

thanks for this detailed explanation!

Last updated: Dec 20 2023 at 11:08 UTC