Writing readable uncluttered group theory

Stream: maths

[Kevin Buzzard]

I noticed that the definition of a group in Lean was one more axiom than it could be

[Kevin Buzzard]

you can prove mul_one from the other axioms

[Kevin Buzzard]

This may well have been talked about before

[Kevin Buzzard]

But I thought I'd write a blog post on this

[Kevin Buzzard]

and I wanted to talk about the proof of mul_one (which goes via mul_left_cancel)

[Kevin Buzzard]

for Lean-groups-without-mul_one

[Kevin Buzzard]

But I could not make the arguments look beautiful

[Kevin Buzzard]

This is kind of OK

[Kevin Buzzard]

lemma gripe.mul_left_cancel {G : Type} [has_mul G] [has_one G] [has_inv G] [gripe G]
: ∀ (a b c : G), a * b = a * c → b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b : (one_mul b).symm
           ... = (a⁻¹ * a) * b : by rw [←gripe.mul_left_inv a]
           ... = a⁻¹ * (a * b) : mul_assoc _ _ _
           ... = a⁻¹ * (a * c) : by rw Habac
-- ... = c : by simp only [mul_assoc,one_mul,mul_left_inv] -- fails
           ... = (a⁻¹ * a) * c : (gripe.mul_assoc _ _ _).symm
           ... = 1 * c : by rw [gripe.mul_left_inv a]
           ... = c : one_mul _
end

[Kevin Buzzard]

although all this has_mul stuff is both really cluttering things up and not actually telling us the one useful thing about it, which is that it is a map alpha -> alpha -> alpha

[Kevin Buzzard]

I made a type for that

[Kevin Buzzard]

class gripe (G : Type) [has_mul G] [has_one G] [has_inv G] :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

[Kevin Buzzard]

But got a bit sick about still having to say we have a has_mul. On the other hand I really want the notation.

[Reid Barton]

can you use extends instead of those extra parameters to the class? I've never used it myself but I see it in the algebraic classes

[Kevin Buzzard]

Other complains about that calc proof is that I need to give too many hint, I seem to have to mention the type's name (gripe) randomly and I can only sometimes get away with _s, and why do I even have to put them at all?

[Kevin Buzzard]

I tried without the structure

[Kenny Lau]

This may well have been talked about before

https://gitter.im/leanprover_public/Lobby?at=59fd723d976e63937e268f50

[Kevin Buzzard]

lemma mul_left_cancel' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)
: ∀ (a b c : G), a * b = a * c → b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b : (one_mul _).symm
           ... = (a⁻¹ * a) * b : by rw [mul_left_inv]
           ... = a⁻¹ * (a * b) : mul_assoc _ _ _ -- why not just mul_assoc?
           ... = a⁻¹ * (a * c) : by rw Habac
-- ... = c : by simp only [mul_assoc,one_mul,mul_left_inv] -- fails
           ... = (a⁻¹ * a) * c : (mul_assoc _ _ _).symm
           ... = 1 * c : by rw [mul_left_inv]
           ... = c : one_mul _ -- why the _ ?
end

[Kevin Buzzard]

and that seemed to go better, but then

[Kevin Buzzard]

theorem mul_one' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)
: ∀ (a : G), a * 1 = a :=
begin
intro a,
 apply (mul_left_cancel' mul_assoc one_mul mul_left_inv a⁻¹ _ _), -- aargh
 rw [←mul_assoc,mul_left_inv,one_mul],
end

[Kenny Lau]

@Kevin Buzzard edit > change title

[Reid Barton]

Oh, I guess you are complaining about has_mul being opaque to the reader wherever it appears, not that you had to write it twice?

[Kevin Buzzard]

I couldn't apply the theorem I proved without carrying around all the axioms.

[Kenny Lau]

wrong thread

[Kevin Buzzard]

I want to write a blog post which looks good and works in Lean and proves clearly that one of the axioms of a group follows from the others

[Kenny Lau]

god

[Kevin Buzzard]

but I really want the kids to understand that they can also do some of their group theory example sheets in Lean

[Kenny Lau]

whatever

[Reid Barton]

How do you feel about using variables instead?

[Kevin Buzzard]

can I move this?

[Kenny Lau]

@Scott Morrison sorry, had to move your messages as well; could you move your messages back to "notations in category theory"?

[Kevin Buzzard]

Sorry

[Kevin Buzzard]

The stupidity of all the has_one has_mul stuff

[Kevin Buzzard]

is that these typeclasses have notation attached to them

[Kevin Buzzard]

and you want to use the notation

[Reid Barton]

variable {G : Type}
variable (mul : G → G → G)
variable (one : G)
variable (inv : G → G)

local notation a `*` b := mul a b
local notation 1 := one
local notation a `⁻¹` := inv a

variable (mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
variable (one_mul : ∀ (a : G), 1 * a = a)
variable (mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

lemma mul_left_cancel' : ∀ (a b c : G), a * b = a * c → b = c :=

[Kevin Buzzard]

Maybe instead of local notation I can use instances

[Reid Barton]

oh, I forgot variables don't get along well with tactics

[Kevin Buzzard]

I am just going to bite the bullet and implement it in 5 different ways and see which one is best

[Kevin Buzzard]

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

[Kevin Buzzard]

Does that class exist @Mario Carneiro ?

[Kevin Buzzard]

It seems to come with free and painless type class inference

[Kevin Buzzard]

I had not appreciated how that barrage of classes in core.lean was actually just a barrage of notation. Each typeclass corresponds to precisely one piece of notation. I had not realised this before!

[Kevin Buzzard]

I don't really understand notation and don't use any in my schemes work.

[Kevin Buzzard]

actually I think I suddenly understand it a whole lot better

[Kevin Buzzard]

my class corresponds to a finite set of notations.

[Kevin Buzzard]

class group' (G : Type) extends has_group_notation G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

[Kevin Buzzard]

@Reid Barton

[Kevin Buzzard]

That's the way to get rid of all that continually carrying around [has_add]

[Kevin Buzzard]

lemma group'.mul_left_cancel {G : Type} [group' G]
: ∀ (a b c : G), a * b = a * c → b = c := sorry

[Kevin Buzzard]

This thread is about making the proof that one of the axioms of a group as defined by Lean follows from all of the others

[Kevin Buzzard]

look as nice and uncluttered as possible

[Kevin Buzzard]

The strat is : first prove mul_left_cancel (without using mul_one of course), and then deduce mul_one. I know there are other strategies but that's the strategy I'd like to showcase in Lean

[Kevin Buzzard]

so I can show the undergraduates one way of revising for their upcoming group theory exam

[Kevin Buzzard]

I want to show them that using Lean to do abstract basic chase stuff around stuff in group theory is really easy in Lean

[Kevin Buzzard]

I'll blog about it but I need to get it as nice looking as possible first

[Kevin Buzzard]

https://gist.github.com/kbuzzard/2adf2b42a9ea23dabc2eb26a1a4b20fb

[Kevin Buzzard]

My efforts using classes

[Kevin Buzzard]

I had to keep writing the class name

[Kevin Buzzard]

and the calc proof needed a lot of blanks

[Kevin Buzzard]

How could this be improved?

[Kevin Buzzard]

I am going to try other ways of setting this up to see pros and cons

[Kenny Lau]

Change

(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))

to

(mul_assoc : ∀ {a b c : G}, a * b * c = a * (b * c))

[Kevin Buzzard]

Do you think that's right?

[Kevin Buzzard]

I changed it for the constants example

[Kevin Buzzard]

and my tactic proof got worse

[Kenny Lau]

if you change it then you don't need to put underscores

[Kevin Buzzard]

I'll show you you're wrong

[Kevin Buzzard]

https://github.com/kbuzzard/xena/blob/master/canonical_isomorphism/group_axioms_constants.lean

[Kevin Buzzard]

But maybe you can fix it :-)

[Kevin Buzzard]

there is a point in tactic mode where I needed underscores :-(

[Kenny Lau]

where?

[Kevin Buzzard]

https://github.com/kbuzzard/xena/blob/master/canonical_isomorphism/group_axioms_class.lean

[Kevin Buzzard]

not there

[Kenny Lau]

so where am I wrong?

[Kevin Buzzard]

https://github.com/kbuzzard/xena/blob/48ce83d8bc9782a08ee852d126e784f696086846/canonical_isomorphism/group_axioms_constants.lean#L48

[Kevin Buzzard]

there

[Reid Barton]

In the calc proof, if you just begin every justification with by rw, you can make it quite uniform (at least in this case)

  exact calc b = 1 * b         : by rw group'.one_mul
           ... = (a⁻¹ * a) * b : by rw group'.mul_left_inv
           ... = a⁻¹ * (a * b) : by rw group'.mul_assoc
           ... = a⁻¹ * (a * c) : by rw Habac
           ... = (a⁻¹ * a) * c : by rw group'.mul_assoc
           ... = 1 * c         : by rw group'.mul_left_inv
           ... = c             : by rw group'.one_mul

[Kenny Lau]

Change

lemma mul_left_cancel : ∀ {a b c : G}, a * b = a * c → b = c :=

to

lemma mul_left_cancel : ∀ (a) {b c : G}, a * b = a * c → b = c :=

[Kevin Buzzard]

do you feel that this change is actually justified rather than it being an attempt to sort out a problem?

[Kenny Lau]

yes, because a could not be infered from the final type b = c

[Kevin Buzzard]

yes

[Kevin Buzzard]

I wondered if that was a reasonable justification for the change

[Chris Hughes]

It can be inferred from the hypothesis though.

[Kevin Buzzard]

exactly

[Kenny Lau]

well if you don't want to change it you can state the hypothesis explicitly using have

[Reid Barton]

... = (a⁻¹ * a) * b : by rw [mul_left_inv] -- why does that line even work? I believe it should fail. Is it a bug?

I was puzzled by this too up until quite recently. The reason it works is that rw does not rewrite the left hand side to the right hand side as one might think. Rather, it rewrites the desired equality 1 * b = (a⁻¹ * a) * b to whatever it becomes after the rewrite, and that rewrite might occur on either side.

[Kevin Buzzard]

so Kenny based on your logic what are the forms of the other axioms that I should be using?

[Reid Barton]

Then because the rewritten goal is of the form a = a, it gets solved by rfl automatically

[Kenny Lau]

@Kevin Buzzard maybe don't make a explicit afterall, lol

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I don't quite know what I am looking for here. I guess what is going on is that different conventions produce different results which may or may not have slight annoyances

[Reid Barton]

Also if you use by rw on every line of the calc proof, then it doesn't matter whether you make the arguments of the axioms explicit or not

[Kevin Buzzard]

Kenny in none of the standard typeclasses do I see variables in axioms being introduced with {}. I am imagining there is a good reason for this

[Kevin Buzzard]

Letting them all be {} announces that you're 100 percent convinced that unification will save you

[Kenny Lau]

well they have interface like

class semigroup (α : Type u) extends has_mul α :=
(mul_assoc : ∀ a b c : α, a * b * c = a * (b * c))

lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) :=
semigroup.mul_assoc

[Kevin Buzzard]

but letting them all be () does not mean you're giving up home

[Kenny Lau]

oh wait

[Kevin Buzzard]

because other things might fill in the gaps later

[Kenny Lau]

right, you still need _ for mul_assoc lol

[Kenny Lau]

so maybe change back to () and use Reid's approach

[Kevin Buzzard]

Sometimes I did

[Kevin Buzzard]

sometimes I didn't

[Kevin Buzzard]

Oh I make the interface!

[Kenny Lau]

I'm saying, the interface in the library still uses explicit variables

[Kevin Buzzard]

exact calc b = 1 * b : by rw group'.one_mul -- that "shouldn't work" either

[Kenny Lau]

why not?

[Kenny Lau]

the goal is b = 1 * b

[Kevin Buzzard]

Oh I see

[Kevin Buzzard]

of course

[Kevin Buzzard]

Kenny do you understand why that bug is not a bug?

[Kevin Buzzard]

line 33

[Kevin Buzzard]

Oh I now understand

[Kevin Buzzard]

I should think of what the rw actually does

[Kevin Buzzard]

not what I want it to do

[Kevin Buzzard]

lemma mul_left_cancel : ∀ {a b c : G}, a * b = a * c → b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b         : by rw one_mul
           ... = (a⁻¹ * a) * b : by rw mul_left_inv
           ... = a⁻¹ * (a * b) : by rw mul_assoc
           ... = a⁻¹ * (a * c) : by rw Habac
           ... = (a⁻¹ * a) * c : by rw mul_assoc
           ... = 1 * c         : by rw mul_left_inv
           ... = c : one_mul
end

[Kevin Buzzard]

Yes that's really nice

[Kevin Buzzard]

That's just how a mathematician would explain it

[Kevin Buzzard]

"apply this axiom"

[Kevin Buzzard]

"I don't care which way"

[Kevin Buzzard]

"the obvious way"

[Kenny Lau]

I'm sure you can have fewer lines lol

[Kevin Buzzard]

of course

[Kevin Buzzard]

but this is the raw beauty which you see here

[Kenny Lau]

and then your begin intros exact kind of defeat the purpose of entering tactic mode

[Kevin Buzzard]

ha ha you are exactly right

[Reid Barton]

I wasn't sure whether to comment about the intros line, haha

[Kenny Lau]

comment about them.

[Kenny Lau]

@Kevin Buzzard I just finished writing a file without ever entering tactic mode

[Kevin Buzzard]

All the rewrites fail in the below

[Kevin Buzzard]

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

structure group' (G : Type) extends has_group_notation G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

variables {G : Type} (group'.G : group' G) [has_group_notation G]
-- variables (H : Type) [has_mul H] [has_one H] [has_inv H]

-- We prove left_mul_cancel for group'

lemma group'.mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : by rw mul_assoc
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc
    ... = 1 * c         : by rw mul_left_inv
                ... = c : by rw one_mul

[Kevin Buzzard]

I am using a structure

[Kevin Buzzard]

I don't understand the error messages

[Kevin Buzzard]

First is

[Kevin Buzzard]

rewrite tactic failed, did not find instance of the pattern in the target expression
  1 * ?m_3
state:
G : Type,
_inst_1 : has_group_notation G,
a b c : G,
Habac : a * b = a * c
⊢ b = 1 * b

[Kevin Buzzard]

I am unimpressed with Lean's instance-finding abilities here

[Kevin Buzzard]

what am i missing?

[Kevin Buzzard]

I wondered how changing a class to astructure changed things

[Kevin Buzzard]

I think all notation as a notational typeclass works great in these sorts of situations

[Kenny Lau]

Lean only finds classes, not structures

[Kevin Buzzard]

it's clear what it's doing

[Kevin Buzzard]

and it's doing nothing more

[Kenny Lau]

the structure isnt even in the hypotheses

[Kevin Buzzard]

I don't understand

[Kevin Buzzard]

I will take notation off

[Kevin Buzzard]

and put pp.all on

[Kevin Buzzard]

am I missing something simple?

[Kevin Buzzard]

kenny can you fix it?

[Kevin Buzzard]

that might help me understand

[Kevin Buzzard]

Look at this beautiful proof

[Kevin Buzzard]

lemma mul_left_cancel' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)
: ∀ (a b c : G), a * b = a * c → b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : by rw mul_assoc
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc
    ... = 1 * c         : by rw mul_left_inv
    ... = c             : by rw one_mul

[Kevin Buzzard]

Can you show me how to make a proof which is just as beautiful, but using a class or structure?

[Kevin Buzzard]

I am getting sick of carrying the axioms around with me

[Kevin Buzzard]

I have packaged up all the notation in a typeclass

[Kevin Buzzard]

but I want to package all the group axioms up as well

[Kevin Buzzard]

The typeclass system is perfect for notation.

[Kevin Buzzard]

There is very little risk of a diamond :-)

[Kevin Buzzard]

I want to package everything away but keep the proof beautiful

[Kevin Buzzard]

and once I have managed that, I think I am done.

[Chris Hughes]

Why aren't you just using the group typeclass?

[Mario Carneiro]

The has_group_notation class has been discussed in some of Jeremy's explorations, called group_struct, but it's not needed in mathlib as it is now

[Mario Carneiro]

The standard way to show that an axiom is redundant is to have an auxiliary constructor for group that doesn't have the redundant axioms

[Chris Hughes]

Is this better?

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

class group' (G : Type) extends has_group_notation G :=
(mul_assoc' : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul' : ∀ (a : G), 1 * a = a)
(mul_left_inv' : ∀ (a : G), a⁻¹ * a = 1)

variables {G : Type} [group' G]
open group'
-- variables (H : Type) [has_mul H] [has_one H] [has_inv H]

-- We prove left_mul_cancel for group'

lemma group'.mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul' b
    ... = (a⁻¹ * a) * b : by rw mul_left_inv'
    ... = a⁻¹ * (a * b) : by rw mul_assoc'
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc'
    ... = 1 * c         : by rw mul_left_inv'
                ... = c : by rw one_mul'

[Chris Hughes]

You had two has_group_notation instances, one from group' and another one

[Kenny Lau]

Just use a namespace and drop the fucking primes

[Chris Hughes]

one mul is global

[Kenny Lau]

protected

[Chris Hughes]

but it doesn't know which one_mul I mean.

[Mario Carneiro]

def group.mk' {α : Type*} [semigroup α] [has_one α] [has_inv α]
  (one_mul : ∀ (a : α), 1 * a = a)
  (mul_left_inv : ∀ (a : α), a⁻¹ * a = 1) : group α :=
have ∀ a : α, a * a = a → a = 1, from λ a h,
  calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
    ... = a⁻¹ * a : by rw [mul_assoc, h]
    ... = 1 : mul_left_inv _,
have ∀ a : α, a * a⁻¹ = 1, from
λ a, this _ $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul],
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := λ a, show a * 1 = a,
    by rw [← mul_left_inv a, ← mul_assoc, this, one_mul],
  ..‹semigroup α›, ..‹has_one α›, ..‹has_inv α› }

[Scott Morrison]

This is a common problem in making definitions --- do you go for maximal axioms (so that you don't need lots of lemmas later, and the big results follow easily from the definitions), or minimal axioms (so instances are easy to construct)? Often, the right solution in Lean is to go for maximal axioms with alternate constructors that require minimal axioms.

[Kevin Buzzard]

The standard way to show that an axiom is redundant is to have an auxiliary constructor for group that doesn't have the redundant axioms

Yes but these are mathematicians with no functional programming background and I think they would prefer to see something which looks like an honest proof (never mention the axiom, then prove it) rather than wrapping anything in a complicated structure.

[Kevin Buzzard]

Mario your proof is in some sense canonical, but I prefer mine for pedagogical reasons.

[Kevin Buzzard]

Just use a namespace and drop the fucking primes

Kenny can you do it? Namespaces seem to lead to overloading anyway.

[Kevin Buzzard]

I am reluctant to prime the axioms

[Kevin Buzzard]

but maybe I have to

[Mario Carneiro]

something which looks like an honest proof (never mention the axiom, then prove it)

I'm confused. Isn't that pretty much exactly what my proof does? I start with a semigroup with a one and inv, and the left_inv and one_mul axioms, and derive mul_one. There is no funny business at all, or complicated structures, it's literally just proving one statement from another, and then wrapping it up in a group. The proof part could also be factored out like so:

section
parameters {α : Type*} [semigroup α] [has_one α] [has_inv α]
  (one_mul : ∀ (a : α), 1 * a = a)
  (mul_left_inv : ∀ (a : α), a⁻¹ * a = 1)
include one_mul mul_left_inv

theorem group.mk'_aux1 {a : α} (h : a * a = a) : a = 1 :=
calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
   ... = a⁻¹ * a : by rw [mul_assoc, h]
   ... = 1 : mul_left_inv _

theorem group.mk'_aux2 (a : α) : a * a⁻¹ = 1 :=
group.mk'_aux1 $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul]

theorem group.mk'_aux3 (a : α) : a * 1 = a :=
by rw [← mul_left_inv a, ← mul_assoc, group.mk'_aux2, one_mul]

def group.mk' : group α :=
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := group.mk'_aux3,
  ..‹semigroup α›, ..‹has_one α›, ..‹has_inv α› }

end

[Mario Carneiro]

Another way to present a proof like this is via an auxiliary class like your gripe, like so:

class gripe (α : Type*) extends semigroup α, has_one α, has_inv α :=
(one_mul : ∀ (a : α), 1 * a = a)
(mul_left_inv : ∀ (a : α), a⁻¹ * a = 1)

namespace gripe
variables {α : Type*} [gripe α]

theorem eq_one_of_idem {a : α} (h : a * a = a) : a = 1 :=
calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
   ... = a⁻¹ * a : by rw [mul_assoc, h]
   ... = 1 : mul_left_inv _

theorem mul_right_inv (a : α) : a * a⁻¹ = 1 :=
eq_one_of_idem $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul]

theorem mul_one (a : α) : a * 1 = a :=
by rw [← mul_left_inv a, ← mul_assoc, mul_right_inv, one_mul]

instance (α) [gripe α] : group α :=
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := mul_one,
  ..gripe.to_semigroup α,
  ..gripe.to_has_one α,
  ..gripe.to_has_inv α }

end gripe

[Kevin Buzzard]

Here's how it ended up. https://xenaproject.wordpress.com/2018/04/30/group-theory-revision/