proving (g⁻¹ * h) * (h⁻¹ * g) = 1 using simp

Stream: general

[Bernd Losert]

MWE:

import tactic
open option

example {G : Type} [group G] : ∀ g h : G, (g⁻¹ * h) * (h⁻¹ * g) = 1 := by simp

Maybe I can't use simp andI have to reassociate things and apply mul_left_inv a bunch of times?

[Yury G. Kudryashov]

by simp [mul_assoc] solves this goal.

[Bernd Losert]

Nice.

[Adam Topaz]

https://leanprover-community.github.io/extras/simp.html

[Adam Topaz]

Learning to effectively use the simplifier is one of the most important things you can do when starting off with lean

[Yury G. Kudryashov]

You can also use assoc_rw here.

[Bernd Losert]

Say I have x * y and I want to insert a 1 in between and expand the 1 into (g⁻¹ * h) * (h⁻¹ * g). This is like the opposite of simp.

[Bernd Losert]

Is this easy to do, or do I have to carefully apply rw?

[Adam Topaz]

Do you know about the rw (show ..., by ...) trick? If not, I can explain a bit later (Christmas is busy around here...)

[Bernd Losert]

I don't think I've seen that. Is it discussed in "Theorem proving in Lean"?

[Bernd Losert]

Hmm.. don't see it there.

[Yaël Dillies]

It's a type-ascription. rw (proof_term : type) will do the same.

[Ruben Van de Velde]

It might be easier to write something like

have : x * y = x * (g⁻¹ * h) * (h⁻¹ * g) * y, { simp },
rw this

[Alex J. Best]

There is also tactic#group btw, under the hood it does something very similar to simp [mul_assoc] but is a nice idiomatic way to solve such goals.

[Yury G. Kudryashov]

You can also use calc mode.

[Adam Topaz]

@Bernd Losert what I had in mind is this:

import algebra
import tactic

example {G : Type*} [group G] (x y z : G) (h : x * y = x * y) : true :=
begin
  rw (show x * y = (x * z) * (z⁻¹ * y), by group) at h,
  sorry,
end

But all the other choices that were mentioned above would work as well.

[Bernd Losert]

I have been using calc mode actually for all this stuff.

[Bernd Losert]

Anyways, thanks a lot for the pointers.