# Zulip Chat Archive

## Stream: new members

### Topic: how do proofs with \< ... \> work?

#### François Sunatori (Jan 22 2021 at 04:37):

Hi, I'm new to Lean.

I saw some examples where

`lemma self_mem_coset (a : G) (H : subgroup G) : a ∈ a ⋆ H := ⟨1, H.one_mem, (group.mul_one a).symm⟩`

.

I'm unsure how to read this proof.

I know that `⟨..., ...⟩`

represents a dependent pair (sigma type) and means that "the type of the second element of the pair, b : β a, depends on the first element of the pair, a : α"

from https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html

What does it translate to in tactics?

Thanks :)

#### Adam Topaz (Jan 22 2021 at 04:39):

Can you say where you found that lemma?

#### Adam Topaz (Jan 22 2021 at 04:40):

Even better, provide a #mwe

#### Adam Topaz (Jan 22 2021 at 04:42):

In any case, the point is that to prove that some element $g$ of a group is a member of a coset associated to $a$, you have to prove that there exists an element $h$ in the subgroup $H$ such that $g = a \cdot h$. In the case $g = a$, you take $h = 1$, so that's the first $1$ appearing there. The `H.one_mem`

is the proof that $1$ is an element of $H$ (which is a subgroup of $G$), while `group.mul_one a`

is the proof that $a = a \cdot 1$, while `symm`

means reverse the equality.

#### Thomas Browning (Jan 22 2021 at 04:42):

A mwe would be helpful, but here's a guess of a tactic proof:

```
begin
use 1,
exact H.one_mem,
exact (group.mul_one a).symm,
end
```

#### François Sunatori (Jan 22 2021 at 04:46):

@Adam Topaz I found it here: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/subgroup/basic.lean#L191

#### François Sunatori (Jan 22 2021 at 04:48):

but how should I interpret the `⟨..., ...⟩`

more generally? Is it just used to sequence terms one after the other? since each spot in the tuple is dependent on the spot before it? (sorry, I don't know if "spot" is the right word to use here)

#### Alex J. Best (Jan 22 2021 at 05:00):

Its called an anonymous constructor, see https://leanprover.github.io/reference/declarations.html#structures-and-records

#### François Sunatori (Jan 22 2021 at 05:03):

Thanks @Alex J. Best ! That's exactly the info I needed. So does this mean that it doesn't correspond to a term of a sigma type?

#### Alex J. Best (Jan 22 2021 at 05:11):

Right, its much more general, you can make terms of sigma types with it like

```
def t : Σ n, vector ℤ n := ⟨0, vector.nil⟩
```

but we can also make a term of type `vector ℤ 1`

with this notation, a vector is a list of a fixed length, so it has one constructor, the list and the proof that it has that length, so this is `⟨[1], by simp⟩ : vector ℤ 1`

. The fun begins when we can combine these:

```
def t' : Σ n, vector ℤ n := ⟨1, ⟨[1], by simp⟩⟩
-- we can remove the nesting which is what makes this notation so powerful:
def t'' : Σ n, vector ℤ n := ⟨1, [1], by simp⟩
```

#### Damiano Testa (Jan 22 2021 at 06:52):

Another place where they can occur is in the proof of iff statements. In this case you would have

```
⟨proof of →, proof of ←⟩
```

#### Kevin Buzzard (Jan 22 2021 at 07:13):

Damiano, you were talking about structures recently -- you can make a term of any structure using this pointy bracket notation. The things in the bracket are the inputs for the constructor.

#### Johan Commelin (Jan 22 2021 at 07:19):

@Damiano Testa Note that `iff`

is just a special case of what Alex said! It's also just a structure (-;

#### Damiano Testa (Jan 22 2021 at 07:29):

Ah, thanks for the information: I did not know that these were all special cases of the same construction!

#### François Sunatori (Jan 22 2021 at 15:43):

In the example shown here https://leanprover.github.io/reference/declarations.html#structures-and-records,

I'm still a little confused as to why `⟨ b₁, b₂, f₁, ..., fₙ ⟩`

is equivalent to `foo.constructor b₁ b₂ f₁ f₁ ... fₙ`

.

My understanding is that a structure is a pi-type with type former : `foo : Π (a : α), Sort u`

Wouldn't a term of the type formed by the structure need to be of a pi-type?

I thought `⟨ ...⟩`

meant it's a term of a sigma-type.

Thanks again!

(I managed to translate a few of the proofs done with `⟨ ...⟩`

into tactic proofs and am getting a better intuition toward it but I think I haven't yet wrapped my head completely around it)

#### Alex J. Best (Jan 22 2021 at 17:22):

The bracket notation is really for any inductive type with only one constructor, check out these examples for instance:

```
inductive foo
| a : foo
#check (⟨⟩ : foo)
inductive bar
| a : bar → bar
variable (l : bar)
#check (⟨⟨⟨l⟩⟩⟩ : bar)
```

#### Eric Wieser (Jan 22 2021 at 17:42):

I think the confusion comes from families of types, but the notation works in the same way:

```
inductive foo (n : nat)
| a : foo
#check (⟨⟩ : foo 3)
```

#### François Sunatori (Jan 22 2021 at 17:59):

ok I'm not sure why I was assuming that `⟨ ...⟩`

was only for sigma types.

I just looked at the sigma type definition (https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/init/core.lean#L247):

```
structure sigma {α : Type u} (β : α → Type v) :=
mk :: (fst : α) (snd : β fst)
```

and it has only one constructor and if I'm not mistaken a `structure`

is an `inductive`

.

This means we can use the "anonymous constructor" `⟨ ...⟩`

to create a term of type `sigma`

.

So if I understood correctly, `⟨ ...⟩`

is not specific to sigma types but instead is specific to inductive types.

#### Eric Wieser (Jan 22 2021 at 18:04):

*with one constructor

#### Eric Wieser (Jan 22 2021 at 18:04):

You can't use it on `or`

, which has two

#### François Sunatori (Jan 22 2021 at 19:16):

thanks @Eric Wieser @Alex J. Best you're explanations really helped me understand this :) and thanks everyone else as well for all your clues to help me untangle this!

Last updated: May 08 2021 at 09:11 UTC