coercion from set to group

Stream: new members

[Kristaps Balodis]

I got stuck trying to reprove the 1-step subgroup test the other day.

import Lean
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Deprecated.Subgroup
import Mathlib.Algebra.Group.Defs


theorem one_step_subgroup_test [Group G] (S : Set G)
(s : S) (h2 : ∀ a b : S, a * (b : G)⁻¹  ∈  S): IsSubgroup S := by
constructor
constructor
have h3 : s⁻¹  : G := by sorry
sorry

sorry

The goal is to show that S has the identity of G . Since I have that s : S I wanted to say that I had its inverse, and then use h3 to get that 1 :S . Is there some conversion trick to remind Lean that ` s : G, or have I made some other egregious error?

[Patrick Massot]

This is a very inconvenient way of stating it. You should start with s having type G and an assumption also for elements of type G.

[Patrick Massot]

Something like

theorem one_step_subgroup_test [Group G] (S : Set G)
{s : G} (hs : s ∈ S) (h2 : ∀ a ∈ S, ∀ b ∈ S, a * b⁻¹  ∈  S): IsSubgroup S :=

[Alex J. Best]

To add to that: you are defining an element of G, which is a term of type G, so the syntax should either state a proposition about that element; e.g.

have h3 : (s : G)⁻¹ ∈ S := sorry

or

let a : G := s⁻¹

if you just want to define the element

[Patrick Massot]

Here is an idiomatic statement and proof in case you are still stuck

solution

import Mathlib.Deprecated.Subgroup

theorem one_step_subgroup_test [Group G] {S : Set G} {s : G} (hs : s ∈ S)
  (h2 : ∀ {a b}, a ∈ S → b ∈ S → a * b⁻¹  ∈  S): IsSubgroup S :=
have one_mem : 1 ∈ S := by simpa using h2 hs hs
have inv_mem : ∀ {a}, a ∈ S → a⁻¹ ∈ S := fun ha ↦ by simpa using h2 one_mem ha
{ one_mem := one_mem
  mul_mem := fun ha hb ↦ by simpa using h2 ha (inv_mem hb)
  inv_mem := inv_mem }

[Kristaps Balodis]

Thanks! It took me a little bit to parse everything, but I found that proof very enlightening, I learned a lot about how things work.

[Kristaps Balodis]

A couple follow-up questions:

1) Is the term "idiomatic" technical here? What would make this proof non-idiomatic?

2) Why did we need import Mathlib.Deprecated.Subgroup as opposed to the other imports I had, and what does "Deprecated" mean in this case?

[Alex J. Best]

IsSubgroup lives in Mathlib.Deprecated.Subgroup, as explained at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Subgroup.html we try to use docs4#Subgroup instead of docs4#IsSubgroup these days, but the deprecated version still lingers around. These things are very similar but packaged up in a different way.
So actually Patrick just minimised your imports to only what was needed.

[Alex J. Best]

Idiomatic doesn't have a technical definition, but it just means things done in a good style to avoid common issues and fit in with the way the rest of the library is written. For example using the structure notation {blah := blah} can be more readable than using the constructor tactic (though you will see both styles in mathlib depending on the context)