Zulip Chat Archive

Stream: new members

Topic: Holes in the goal!


view this post on Zulip 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

view this post on Zulip Alex J. Best (Aug 12 2020 at 01:06):

set_option pp.proofs true

view this post on Zulip 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!))

view this post on Zulip Alex J. Best (Aug 12 2020 at 01:08):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Aug 12 2020 at 02:16):

Have you seen src#category_theory.Aut?

view this post on Zulip Scott Morrison (Aug 12 2020 at 02:17):

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

view this post on Zulip Scott Morrison (Aug 12 2020 at 02:17):

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

view this post on Zulip 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!

view this post on Zulip 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