## Stream: new members

### Topic: Holes in the goal!

#### Pedro Minicz (Aug 12 2020 at 01:04):

I have classical.some _ in my goal! I find myself unable to maneuver around it, although the goal itself should be easy.

Unfortunately my #mwe is a bit big...

import algebra.group

noncomputable theory

section

parameters {α : Type*} [nonempty α]

def iso : Type* := {f : α → α // function.bijective f}

variables {β : Type*} {f : α → β} {g : β → α}

@[simp] def iso.mul : iso → iso → iso :=
λ ⟨f, hf⟩ ⟨g, hg⟩, ⟨f ∘ g, function.bijective.comp hf hg⟩

open function (left_inverse) (right_inverse)

@[simp] lemma function.left_inverse_iff_right_inverse :
left_inverse f g ↔ right_inverse g f :=
⟨function.left_inverse.right_inverse, function.right_inverse.left_inverse⟩

lemma iso.inv (f : iso) :
∃ g : iso, left_inverse g.val f.val ∧ right_inverse g.val f.val :=
begin
cases f with f hf,
rw function.bijective_iff_has_inverse at hf,
cases hf with g hg,
use g,
{ rw function.bijective_iff_has_inverse,
use f,
rwa and.comm },
{ simpa using hg }
end

instance iso.group : group iso :=
{ mul := iso.mul,
mul_assoc := λ ⟨_, _⟩ ⟨_, _⟩ ⟨_, _⟩, by simp,
one := ⟨id, function.bijective_id⟩,
one_mul := λ ⟨_, _⟩, by simp [has_mul.mul],
mul_one := λ ⟨_, _⟩, by simp [has_mul.mul],
inv := λ f, classical.some (iso.inv f),
mul_left_inv :=
begin
unfold has_inv.inv,
sorry
end }

end


#### Alex J. Best (Aug 12 2020 at 01:06):

set_option pp.proofs true

#### Alex J. Best (Aug 12 2020 at 01:07):

Its not a hole, just a proof that lean has elected to hide from you (as it is irrelevant (in the technical sense!))

#### Alex J. Best (Aug 12 2020 at 01:08):

Probably you'll need to use classical.some_spec  somewhere to proceeed

#### Yakov Pechersky (Aug 12 2020 at 02:07):

Here's how far I got, added some more API:

import algebra.group

noncomputable theory

section

parameters {α : Type*} [nonempty α]

def iso : Type* := {f : α → α // function.bijective f}

theorem ext_iff {f g : iso} : (∀ x, f.val x = g.val x) ↔ f = g :=
begin
split,
{ intros h,
apply subtype.eq,
funext,
exact h x },
{ intros h x,
rw h }
end

variables {β : Type*} {f : α → β} {g : β → α}

@[simp] def iso.mul : iso → iso → iso :=
λ ⟨f, hf⟩ ⟨g, hg⟩, ⟨f ∘ g, function.bijective.comp hf hg⟩

@[simp] lemma iso_mul_def (f g : iso) : iso.mul f g = ⟨f.val ∘ g.val, function.bijective.comp f.property g.property⟩ :=
by { obtain ⟨f, hf⟩ := f, obtain ⟨g, hg⟩ := g, simp }

@[simp] lemma iso_mul_val (f g : iso) : (iso.mul f g).val = f.val ∘ g.val := by simp

lemma iso_mul_property (f g : iso) : (iso.mul f g).property = function.bijective.comp (f.mul g).property function.bijective_id := by simp

@[simp] lemma iso_mul_eq_iff (f g h : iso) : f.mul g = h ↔ f.val ∘ g.val = h.val :=
begin
obtain ⟨h, hp⟩ := h,
split,
{ intro hm,
rw iso_mul_def at hm,
exact subtype.mk.inj hm },
{ intro hm,
rw iso_mul_def,
exact subtype.eq hm }
end

open function (left_inverse) (right_inverse)

@[simp] lemma function.left_inverse_iff_right_inverse :
left_inverse f g ↔ right_inverse g f :=
⟨function.left_inverse.right_inverse, function.right_inverse.left_inverse⟩

lemma iso.inv (f : iso) :
∃ g : iso, left_inverse g.val f.val ∧ right_inverse g.val f.val :=
begin
cases f with f hf,
rw function.bijective_iff_has_inverse at hf,
cases hf with g hg,
use g,
{ rw function.bijective_iff_has_inverse,
use f,
rwa and.comm },
{ simpa using hg }
end

instance iso.group : group iso :=
{ mul := iso.mul,
mul_assoc := λ ⟨_, _⟩ ⟨_, _⟩ ⟨_, _⟩, by simp,
one := ⟨id, function.bijective_id⟩,
one_mul := λ ⟨_, _⟩, by simp [has_mul.mul],
mul_one := λ ⟨_, _⟩, by simp [has_mul.mul],
inv := λ f, classical.some (iso.inv f),
mul_left_inv := λ f, by {
rcases (classical.some_spec (iso.inv f)),
simp [has_mul.mul, semigroup.mul, function.comp_app, <-ext_iff],
intros x,
specialize left x,
/-
α : Type u_1,
_inst_1 : nonempty α,
f : iso,
right : right_inverse (classical.some _).val f.val,
x : α,
left : (classical.some _).val (f.val x) = x
⊢ (classical.some _).val (f.val x) = 1.val x
-/
sorry
},

}

end


#### Scott Morrison (Aug 12 2020 at 02:16):

Have you seen src#category_theory.Aut?

#### Scott Morrison (Aug 12 2020 at 02:17):

This builds the automorphism group for any object where there is a category structure.

#### Scott Morrison (Aug 12 2020 at 02:17):

If you have G : Group, then use can just use Aut G.

#### Pedro Minicz (Aug 13 2020 at 00:19):

I managed to complete the proof and it can be seen here. Thanks for everyone who commented!

#### Pedro Minicz (Aug 13 2020 at 00:25):

Also, I found that I was trying to do on mathlib. I believe the mathlib version does not use noncomputable, not sure about choice as I haven't investigated it deeply.

Last updated: May 10 2021 at 19:16 UTC