## 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: May 06 2021 at 20:13 UTC