# Zulip Chat Archive

## Stream: new members

### Topic: Equivalence between subtype and bundled type

#### Nicolò Cavalleri (Aug 29 2020 at 10:19):

In the file `algebra.group.units`

, how can I fill up the sorries of the following definition, placed after `is_unit.unit`

?

```
noncomputable def is_unit.equiv [monoid M] : equiv {a : M | is_unit a} (units M) :=
{ to_fun := λ a, a.prop.unit,
inv_fun := λ a, ⟨a.val, a, rfl⟩,
left_inv := begin intros x, ext, simp only [subtype.coe_mk], sorry end,
right_inv := begin intro x, dsimp only, sorry end }
```

I would expect `refl`

to work, but it is as if Lean is replacing things with underscores and cannot look back in to them.

#### Kenny Lau (Aug 29 2020 at 10:26):

```
import algebra.group.units
import data.equiv.basic
variables (M : Type*)
noncomputable def is_unit.equiv [monoid M] : equiv {a : M | is_unit a} (units M) :=
equiv.symm $ equiv.of_injective _ units.ext
```

#### Kenny Lau (Aug 29 2020 at 10:27):

`{ a | is_unit a }`

is defeq to `set.range (coe : units M -> M)`

#### Nicolò Cavalleri (Aug 29 2020 at 10:55):

Ok thanks a lot! This looks smart, I'll try to understand the proof

#### Kevin Buzzard (Aug 29 2020 at 16:14):

`refl`

doesn't work because "eta isn't refl" I think. For example if z is a complex number, then `\<z.re, z.im\> = z`

but the proof isn't refl, it's `cases z, refl`

. You need to case on x more in your first sorry. That's what the underscores are -- they're parts of x which don't have names yet.

#### Kevin Buzzard (Aug 29 2020 at 16:16):

No, I tell a lie, the issue is that `is_unit`

is an existence statement, and to get the unit there's some `classical.some`

, so your underscore is something which needs to be reasoned about with `classical.some_spec`

. I think Kenny's approach is better.

#### Kevin Buzzard (Aug 29 2020 at 16:18):

```
/-- The element of the group of units, corresponding to an element of a monoid which is a unit. -/
noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : units M :=
classical.some h
lemma is_unit.unit_spec [monoid M] {a : M} (h : is_unit a) : ↑h.unit = a :=
classical.some_spec h
```

If you look at the definition of `is_unit.unit`

in mathlib then immediately afterwards we see the API, i.e. the function you need.

#### Kevin Buzzard (Aug 29 2020 at 16:20):

```
left_inv := begin
change ∀ _, _, -- so rintro? works, but you can comment this line out
rintro ⟨_, ⟨val, inv, h1, h2⟩, rfl⟩, -- using rintro and changing names to shorter ones
ext,
-- dsimp, -- I wrote this line so I could see what the heck was going on, but it's not needed
exact is_unit.unit_spec _,
end,
```

#### Kevin Buzzard (Aug 29 2020 at 16:22):

```
right_inv := begin
rintro ⟨val, inv, h1, h2⟩,
ext,
exact is_unit.unit_spec _,
end }
```

#### Kevin Buzzard (Aug 29 2020 at 16:24):

here is the list of the greek letters involved in "computation" in lambda calculus, and here is the list of the ones which are built into Lean's definition of definitional equality, i.e. the ones which refl works for. The one which is missing is "eta reduction for structures" I think, but I'm certainly not an expert. But in this case the problem was something else anyway, namely the classical issue involved in getting from the existence statement to the actual object.

Last updated: Dec 20 2023 at 11:08 UTC