# Zulip Chat Archive

## Stream: new members

### Topic: long proof for an easy lemma

#### Xavier Xarles (Jul 04 2020 at 12:38):

Hi all. I have an easy lemma on group theory, and a long proof. I am sure there should be a shorter proof.

```
import tactic
import group_theory.subgroup
lemma mem_cancel_subgroup {G : Type*} [comm_group G] (s : subgroup G) {g a : G}(h₁ : a∈ s)(h₂ : g*a∈ s):
g∈ s:=
begin
have a_inv_in_s : a⁻¹ ∈ s, by {rw subgroup.inv_mem_iff, exact h₁},
suffices mess : g*(a⁻¹)⁻¹*a⁻¹ ∈ s, by {rw inv_mul_cancel_right at mess, exact mess},
have h₃ : g*a*a⁻¹ =g*(a⁻¹)⁻¹*a⁻¹ , by group,
have h₄ : g*a*a⁻¹∈ s, by exact s.mul_mem(h₂)(a_inv_in_s),
rw h₃ at h₄,
exact h₄,
end
```

#### Patrick Massot (Jul 04 2020 at 12:41):

```
import tactic
import group_theory.subgroup
lemma mem_cancel_subgroup {G : Type*} [comm_group G] (s : subgroup G) {g a : G}(h₁ : a∈ s)(h₂ : g*a∈ s):
g∈ s:=
begin
library_search,
end
```

#### Xavier Xarles (Jul 04 2020 at 13:07):

Thanks. I should try always library_search !

#### Kevin Buzzard (Jul 04 2020 at 13:12):

Hi @Xavier Xarles by the way! Long time no see. There is an art to using `library_search`

.

#### Kevin Buzzard (Jul 04 2020 at 13:12):

The art is knowing what to expect from the library. For example you might not expect `library_search`

to solve `2 + 2 < 37`

because who would put this in a library? It's a theorem, but it's not worth recording.

#### Kevin Buzzard (Jul 04 2020 at 13:14):

But you can imagine that this cancellation lemma would be part of a tedious collection of lemmas in the library about elements of subgroups -- this is exactly the sort of stuff you'd find in the library.

#### Xavier Xarles (Jul 04 2020 at 20:33):

Thanks @Kevin Buzzard . Now that I learned `library_search`

I am starting to use a lot. I was hoping seeing you in Barcelona. Let's hope sometime in the future...

Last updated: Dec 20 2023 at 11:08 UTC