Holes in the goal!

Stream: new members

[Pedro Minicz]

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]

set_option pp.proofs true

[Alex J. Best]

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]

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

[Yakov Pechersky]

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]

Have you seen src#category_theory.Aut?

[Scott Morrison]

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

[Scott Morrison]

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

[Pedro Minicz]

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

[Pedro Minicz]

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.