long proof for an easy lemma

Stream: new members

[Xavier Xarles]

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]

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]

Thanks. I should try always library_search !

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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...