Why is g*h=g*h unresolved with an extra hypothesis?

Stream: general

[Phil Wood]

I taught a Introduction to Lean 3 course this semester, and one student came upon an odd issue using quotient groups. The student reduced one part of a proof to showing that
g * h = g * h
which ought to be true by reflexivity; however, this was prevented from happening due to the hypothesis [group (G / N)]. I think the hypothesis [group (G/N)] is redundant, since G/N is a group by virtue of N being a normal subgroup and the definition of taking the quotient group. (Then again, group G doesn't type check as Prop, so I am not entirely sure what having [group (G/N)] as a hypothesis means.) In any case, removing the hypothesis [group (G/N)] makes everything work (i.e., the goal below closes, and the sorry is not necessary), and I would be curious if there is a nice way to explain this behavior.

Below is code replicating the issue.

import data.real.basic
import group_theory.quotient_group


variables (G : Type*) [group G]
          (N : subgroup G) (hN : subgroup.normal N)

def quot_map :=
  @quotient_group.mk' _ _ (N) (hN)
#check quot_map G
#check quot_map G N hN

example
    [group (G ⧸ N)]
    (g h : G ⧸ N)
    (g' h' : G)
    (hh': (quot_map G N hN) h' = h)
    (hg': (quot_map G N hN) g' = g)
    : (quot_map G N hN) (g' * h') = g * h
  :=
begin
  rw [monoid_hom.map_mul, hh', hg'],
  /- The remaining goal is
      ⊢ g * h = g * h
     If the hypothesis [group (G / N)] is
     commented out, the goal closes automatically,
     but it does not if the hypothesis
     "[group (G / N)]" is left in.  Why is that?
  -/
  sorry,
end

[Yaël Dillies]

Write set_option pp.all true at the top of the file and you will see that the two g * h are not the same.
One is the sensible one coming from the multiplication on g. The other one is an arbitrary multiplication introduced by your extraneous [group (G / N)].

[Patrick Massot]

Phil, are your group theory exercises available somewhere?

[Kevin Buzzard]

[group (G / N)] means "let us now put a totally arbitrary group structure on $G/N$ which is unrelated to the one you're thinking of"

[Kevin Buzzard]

like (G : Type) [group G] means "let G be a set, and then let's put a totally arbitrary group structure on G which we know nothing about (but now things like 1 : G make sense, when they didn't before)"

[Phil Wood]

This is super helpful! So that hypothesis [group (G/N)] is doing something new (and problematic!) to the proof state. And I can indeed see the different multiplication being used with the set_option pp.all true.

Patrick—I don't have any particular group theory exercises. A few students did final projects for the course involving groups, for example this particular student was working to implement the statement "If N is a normal subgroup of G, then G/N is abelian if and only if [G,G] is contained in N." And by now, those students have a better understanding of the group theory libraries than I do!

[Kevin Buzzard]

Lean's typeclass inference system should find the term of type group (G / N) automatically, it's not your job to make a term of this type. Looking in the library file for quotient groups I can see it's called docs#quotient_group.quotient.group , and following that link I see that the typeclass inference system is expecting to find [N.normal]. This tells me that subgroup.normal is actually a class, so you would probably be better off writing [hN : subgroup.normal N](or, using dot notation, [hN : N.normal]) so that the typeclass inference system knows that the subgroup is normal.

[Kevin Buzzard]

docs#quotient_group.mk'

[Kevin Buzzard]

Aha, that function also expects the typeclass inference system to find the proof of normality, so you wouldn't need the @ in the definition of quot_map if you'd put hN into the system. Indeed, if you open quotient_group then you don't even need to define quot_map at all, you can just call it mk' N and it should work fine.