# Zulip Chat Archive

## Stream: new members

### Topic: problem trying to prove instance comm_group

#### Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:20):

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 (Jun 12 2020 at 18:23):

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 (Jun 12 2020 at 18:23):

that would be a problem ;-)

#### Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:24):

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

#### Kevin Buzzard (Jun 12 2020 at 18:24):

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

#### Kevin Buzzard (Jun 12 2020 at 18:25):

I get `unknown identifier 'normal_subgroup'`

. I'm using today's mathlib. -- Aah, I need to add `import deprecated.subgroup`

#### Kevin Buzzard (Jun 12 2020 at 18:28):

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 (Jun 12 2020 at 18:29):

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

#### Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:36):

But anyway, change helped me already, thanks

#### Johan Commelin (Jun 12 2020 at 18:43):

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

#### Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:47):

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 (Jun 12 2020 at 18:50):

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 (Jun 12 2020 at 18:51):

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 (Jun 12 2020 at 18:58):

thanks

#### Bryan Gin-ge Chen (Jun 12 2020 at 18:59):

Here's the tactic doc: tactic#change

#### Carl Friedrich Bolz-Tereick (Jun 13 2020 at 06:48):

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

Last updated: Dec 20 2023 at 11:08 UTC