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