Zulip Chat Archive

Stream: new members

Topic: long proof for an easy lemma


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Xavier Xarles (Jul 04 2020 at 13:07):

Thanks. I should try always library_search !

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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