problem trying to prove instance comm_group

Stream: new members

[Carl Friedrich Bolz-Tereick]

I am a total Lean newbie, so maybe I am trying something too advanced, but anyway: I was trying to prove that a normal subgroup of a group is a commutative group. I am running into some problem with coercions (or my understanding of type classes is wrong, I can't quite tell). What I tried is this:

import group_theory.subgroup

variables (G : Type*) [group G]

instance normal_subgroup_is_comm_group (s: set G) [normal_subgroup s] : comm_group s := {
    mul_comm := begin
        -- here * is not expanded
        rintros ⟨a, ha⟩ ⟨b, hb⟩,
        simp, -- can't simplify the definition of *, for some reason?!
        sorry,
    end,
    mul_assoc := begin -- part of ..subtype.group, but I include it to show the difference to mul_comm
        -- here the definition of * from subtype.monoid (via subtype.group) is used
        rintros ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩,
        simp, -- simplifies the definition of * just fine
        exact mul_assoc a b c,
    end,
    ..subtype.group
}

[Kevin Buzzard]

One issue here is the fact that it's not true that an arbitrary normal subgroup of an arbitrary group is always commutative.

[Carl Friedrich Bolz-Tereick]

that would be a problem ;-)

[Carl Friedrich Bolz-Tereick]

but I still don't understand why the first simp doesn't manage to expand *

[Kevin Buzzard]

In fact I think this might be the only issue, you seem to have proved associativity just fine

[Kevin Buzzard]

I get unknown identifier 'normal_subgroup'. I'm using today's mathlib. -- Aah, I need to add import deprecated.subgroup

[Kevin Buzzard]

So your goal is ⊢ ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨b, hb⟩ * ⟨a, ha⟩ and simp doesn't do anything -- I don't understand the question. You want to change it to a * b = b * a? This works:

        rintros ⟨a, ha⟩ ⟨b, hb⟩,
        change (⟨a * b, _⟩ : s) = ⟨b * a, _⟩,
        simp,

[Carl Friedrich Bolz-Tereick]

I don't understand why the second simp does something, and the first doesn't

[Carl Friedrich Bolz-Tereick]

But anyway, change helped me already, thanks

[Johan Commelin]

@Carl Friedrich Bolz-Tereick Are you thinking of "a subgroup of a commutative group is always normal"?

[Carl Friedrich Bolz-Tereick]

no, I arrived at this mathematically wrong example above while trying to reduce more and more what I actually tried to prove, which is that the center of a division_ring is a comm_ring. with kevin's hint I now managed to do that. I don't completely understand how the change tactic he proposed works, though

[Kevin Buzzard]

The second simp doesn't do anything useful. * is notation for has_mul.mul which simp has changed to the definitionally equal group.mul.

[Kevin Buzzard]

If the goal is X then change Y will successfully change the goal to Y if and only if X and Y are definitionally equal.

[Carl Friedrich Bolz-Tereick]

thanks

[Bryan Gin-ge Chen]

Here's the tactic doc: tactic#change

[Carl Friedrich Bolz-Tereick]

and I managed to show that the center of a division_ring is a field, which is what I originally wanted to try :-). the proof is pretty hairy though, need to simplify it