## 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: May 16 2021 at 05:21 UTC