Puzzling error message

Stream: new members

[Walter Moreira]

This simple example does not compile and it shows a puzzling error message. The error message says that it cannot unify g * h = h * g with g * h = h * g. What am I doing wrong?

import tactic

example (G : Type*) [group G] [comm_group G] :
  ∀ g h : G, g * h = h * g :=
begin
intros,
apply mul_comm g h,
end

Screen-Shot-2020-06-12-at-9.03.50-PM.png

[Mario Carneiro]

whenever you see an error like that turn up the printing options

[Mario Carneiro]

set_option pp.all true

[Mario Carneiro]

In the error message you will see that it is trying to unify something about the inst_1 group to something about the inst_2 group

[Mario Carneiro]

You have endowed G with two incompatible group structures with your assumptions

[Walter Moreira]

Ah yes! Makes total sense. A bit difficult to read the error message with the full options, but I can see that now.

[Walter Moreira]

Following up on this, I'm confused about something that gives me an "extra" structure (which was what I was trying to #mwe before):

import tactic
import group_theory.order_of_element

example (G : Type*) [group G] [is_cyclic G]:
  ∀ g h : G, g * h = h * g :=
begin
intros,
have z := @is_cyclic.comm_group G _inst_1 _inst_2,
sorry
end

How do I use the mul_comm property of z to prove the goal? Every attempt seems to produce those two different structures in G that don't unify.

[Mario Carneiro]

Use letI

[Mario Carneiro]

example (G : Type*) [group G] [is_cyclic G]:
  ∀ g h : G, g * h = h * g :=
begin
  intros,
  letI := @is_cyclic.comm_group G _inst_1 _inst_2,
  apply mul_comm
end

[Mario Carneiro]

letI does two things: it inserts a let into the context, and it adds that new variable to the typeclass search so that mul_comm picks it up

[Mario Carneiro]

it is essential that it be a let and not a have so that lean can verify that the group structure on G here is defeq to the original group structure on G

[Walter Moreira]

Oh, I see. I guess these are the docs https://leanprover-community.github.io/mathlib_docs/tactics.html#Instance%20cache%20tactics, right? I missed that.

Thanks so much!