# Zulip Chat Archive

## Stream: new members

### Topic: Frustration with finset

#### Marc Masdeu (Jul 02 2020 at 14:14):

Hi all,

Noob question: I am trying to prove some elementary results in number theory to get more practice with Lean proof writing. I feel that some generic tactic should kill this MWE, but I can't seem to find it:

```
import group_theory.subgroup
import tactic
open_locale classical big_operators
lemma blah {G : Type*} [comm_group G] [fintype G]:
(∏ g : G, g) = (∏ g in {g : G | true}.to_finset, g) :=
begin
sorry,
end
```

Thanks in advance for any help...

#### Mario Carneiro (Jul 02 2020 at 14:26):

`congr, ext, simp`

#### Johan Commelin (Jul 02 2020 at 14:27):

@Marc Masdeu Hi, welcome back. (Have you seen https://leanprover-community.github.io/lftcm2020/)

Ooh, Mario is faster with answering the actual question :oops:

#### Marc Masdeu (Jul 02 2020 at 14:33):

Marc Masdeu Hi, welcome back. (Have you seen https://leanprover-community.github.io/lftcm2020/)

Thanks @Johan Commelin, I've been following everything Lean, just not posting to here... I know about the workshop, but sadly I'll be "away" next week...

#### Johan Commelin (Jul 02 2020 at 14:34):

Ok, no worries!

#### Marc Masdeu (Jul 02 2020 at 14:50):

OK, turns out that the MWE I constructed was too M (but thanks @Mario Carneiro ! I did learn about congr!). Here's an updated one, hopefully it is enough now:

```
def some_subgroup (G : Type*)[comm_group G] : subgroup G := sorry
lemma blah2 {G : Type*} [comm_group G] [fintype G]:
(∏ (x : G) in {x : G | x ∈ some_subgroup G}.to_finset, x) =
∏ (g : ↥(some_subgroup G)), ↑g :=
begin
sorry,
end
```

#### Johan Commelin (Jul 02 2020 at 14:53):

```
apply finset.prod_congr --?
```

#### Marc Masdeu (Jul 02 2020 at 14:57):

It complains with

```
invalid apply tactic, failed to unify
∏ (x : G) in {x : G | x ∈ some_subgroup G}.to_finset, x = ∏ (g : ↥(some_subgroup G)), ↑g
with
?m_4.prod ?m_5 = ?m_6.prod ?m_7
```

#### Johan Commelin (Jul 02 2020 at 14:57):

Aah, of course

#### Johan Commelin (Jul 02 2020 at 14:58):

The rhs is over some subgroup.

#### Johan Commelin (Jul 02 2020 at 14:58):

`rw finset.prod_subtype`

?

#### Johan Commelin (Jul 02 2020 at 14:58):

If all else fails, there is `finset.prod_bij`

but I would try to avoid that.

#### Marc Masdeu (Jul 02 2020 at 15:00):

`finset.prod_subtype`

does not seem to exists...

#### Johan Commelin (Jul 02 2020 at 15:00):

`import data.fintype.card`

? I think

#### Marc Masdeu (Jul 02 2020 at 15:04):

This has worked:

```
rw finset.prod_subtype,
tauto,
finish,
```

Leaving me with no idea of what's going on, of course...

#### Mario Carneiro (Jul 02 2020 at 15:05):

`prod_subtype`

is missing

#### Mario Carneiro (Jul 02 2020 at 15:11):

oops, misread Johan's suggestion. This proof might be a little clearer:

```
lemma blah2 {G : Type*} [comm_group G] [fintype G]:
(∏ (x : G) in {x : G | x ∈ some_subgroup G}.to_finset, x) =
∏ (g : ↥(some_subgroup G)), ↑g :=
begin
apply finset.prod_subtype,
simp, exact λ _, iff.rfl
end
```

#### Mario Carneiro (Jul 02 2020 at 15:13):

Unfortunately the unification problem leaves `has_coe_t_aux.coe`

in the term, and `simp`

doesn't know how to simplify it, so we have to finish with `iff.rfl`

instead

#### Marc Masdeu (Jul 02 2020 at 17:25):

Here is what I have managed to prove: given a finite commutative group G, the product of all its elements equals the product of its elements of order 2. This could be seen as some sort of generalization of Wilson's theorem on the factorial of p-1 modulo p.

Now I know that this is terrible coding style, especially the proof of `prod_all_eq_prod_two_torsion`

. I would appreciate a constructive critique of it. I am not looking for anything mathlib-ready at all, and in fact I'm happy with expensive tactics (to prove mathematically obvious statements) as long as it stays somewhat readable...

Thanks!

```
import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic
open_locale classical big_operators
lemma prod_finset_distinct_inv {α : Type*} [comm_group α] {s : finset α} :
(∀ x ∈ s, x⁻¹ ∈ s) → (∀ x ∈ s, x⁻¹ ≠ x) → (∏ x in s, x) = 1 :=
begin
apply finset.case_strong_induction_on s, by tauto,
intros a s a_notin_s H h1 h2,
specialize H (finset.erase s a⁻¹) (finset.erase_subset (a⁻¹) s),
have r : (∏ x in (finset.erase s a⁻¹), x) = 1,
{
apply H,
{
intros x h,
suffices : ¬x = a ∧ x⁻¹ ∈ s, by simpa,
split,
clarify,
suffices : x⁻¹ ≠ a, by finish,
have x_not_ainv := finset.ne_of_mem_erase h,
by_contradiction hh,
push_neg at hh,
induction hh,
finish,
},
{
intros x h,
apply h2,
exact finset.mem_insert_of_mem (finset.mem_of_mem_erase h)
}
},
{
rw finset.prod_insert a_notin_s,
suffices hkey : (∏ x in s, x) = a⁻¹,
exact mul_eq_one_iff_inv_eq.mpr (eq.symm hkey),
have ainv_notin_s1 : a⁻¹ ∉ finset.erase s a⁻¹ := finset.not_mem_erase a⁻¹ s,
have ainv_in_s : a⁻¹ ∈ s,
{
have ainv_in_s1 : a⁻¹ ∈ insert a s := h1 a (finset.mem_insert_self a s),
suffices : a⁻¹ ≠ a, by exact finset.mem_of_mem_insert_of_ne ainv_in_s1 this,
exact h2 a (finset.mem_insert_self a s)
},
{
rw [←finset.insert_erase ainv_in_s,finset.prod_insert ainv_notin_s1,r],
exact mul_one a⁻¹
},
},
end
def two_torsion_subgroup (G : Type*)[comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := by simp,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
begin
tidy,
rw [mul_mul_mul_comm a b a b, ha, hb],
refine mul_one 1,
end,
inv_mem' := λ a (ha : a * a = 1), by {tidy, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha}
}
lemma prod_all_eq_prod_two_torsion {G : Type*} [comm_group G] [fintype G]:
(∏ g : G, g) = (∏ g : two_torsion_subgroup G, g) :=
begin
have hdisj : disjoint {x : G | x ∈ two_torsion_subgroup G} {x : G | x ≠ x⁻¹ },
{
intros x hx,
cases hx with h1 h2,
norm_num,
have hA : x * x = 1, by assumption,
suffices hB : x * x ≠ 1, by exact h2 (false.rec (x = x⁻¹) (hB hA)),
clear hA h1,
simp [← mul_eq_one_iff_eq_inv] at h2,
assumption,
},
have h : (∏ g in {x : G | x ≠ x⁻¹ }.to_finset, g) = 1,
{
apply prod_finset_distinct_inv;
finish,
},
have H : (∏ (g : G), g) = (∏ x in {x : G | x ∈ two_torsion_subgroup G}.to_finset, x)
* (∏ x in {x : G | x ≠ x⁻¹ }.to_finset, x),
{
--simp [finset.prod_union],
simp at *,
rw ← finset.prod_union,
{
congr,
ext1,
simp [finset.coe_inj],
safe,
suffices hh : a ∈ two_torsion_subgroup G, tauto,
have a2: a * a = 1 := eq_inv_iff_mul_eq_one.mp h_1,
tauto,
},
{
simp [finset.disjoint_iff_disjoint_coe],
exact hdisj,
}
},
{
rw [H, h],
simp at *,
apply finset.prod_subtype,
finish,
},
end
```

#### Alex J. Best (Jul 02 2020 at 20:41):

Its a nice result, I'd say we should have (some version) it in mathlib!

I made some comments inline: it looks pretty good to me, maybe more lemmas and less long proofs would be more manageable though, like for the last statement you could have a lemma that

prod of elements of G is prod of the two torsion times prod of things not their own inverse.

then a lemma that the prod of things that are not their own inverse of any group is one, all as separate lemmas which are combined at the end (basically all of the have's in the last proof could be lemmas)

```
import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic
open_locale classical big_operators
/- General comments
1. You can add @[to_additive] to generate additive versions of these lemmas if you like
2. you use tactics like clarify, finish, safe, a lot, these things can be a little slow, but they
are convenient, so might be best to separate out some of the times they are used as separate lemmas
whose proof is just by finish or whatever, so that they don't get re-run all the time -/
set_option profiler true -- you can use this too see time spent on proofs
lemma prod_finset_distinct_inv {α : Type*} [comm_group α] {s : finset α} :
(∀ x ∈ s, x⁻¹ ∈ s) → (∀ x ∈ s, x⁻¹ ≠ x) → (∏ x in s, x) = 1 :=
begin
apply finset.case_strong_induction_on s, by tauto,
intros a s a_notin_s H h1 h2,
specialize H (finset.erase s a⁻¹) (finset.erase_subset (a⁻¹) s),
have r : (∏ x in (finset.erase s a⁻¹), x) = 1,
{
apply H,
{
intros x h,
suffices : ¬x = a ∧ x⁻¹ ∈ s, by simpa,
split,
begin finish, end, -- this takes ages
suffices : x⁻¹ ≠ a, from finset.mem_of_mem_insert_of_ne (h1 x (finset.mem_insert_of_mem (finset.mem_of_mem_erase h))) this,
-- replaced finish with an explicit proof,
by_contradiction hh,
push_neg at hh,
induction hh,
simpa using finset.ne_of_mem_erase h,
-- replaced finish with an explicit proof and don't name a short term that is only used once now
},
{
intros x h,
apply h2,
exact finset.mem_insert_of_mem (finset.mem_of_mem_erase h)
}
},
{
rw finset.prod_insert a_notin_s,
suffices hkey : (∏ x in s, x) = a⁻¹,
exact mul_eq_one_iff_inv_eq.mpr (eq.symm hkey),
have ainv_notin_s1 : a⁻¹ ∉ finset.erase s a⁻¹ := finset.not_mem_erase a⁻¹ s,
have ainv_in_s : a⁻¹ ∈ s,
{
have ainv_in_s1 : a⁻¹ ∈ insert a s := h1 a (finset.mem_insert_self a s),
suffices : a⁻¹ ≠ a, from finset.mem_of_mem_insert_of_ne ainv_in_s1 this, -- by exact can almost always be removed!
-- as it is just openening tactic mode then returning to term mode
exact h2 a (finset.mem_insert_self a s)
},
{
rw [←finset.insert_erase ainv_in_s,finset.prod_insert ainv_notin_s1,r],
exact mul_one a⁻¹
},
},
end
def two_torsion_subgroup (G : Type*) [comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := by simp,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
begin
dsimp, -- use tidy? and tidy will tell you what it did in this case it only did dsimp at *, and we can just change it to dsimp
rw [mul_mul_mul_comm a b a b, ha, hb],
exact mul_one 1, -- exact instead of refine
end,
inv_mem' := λ a (ha : a * a = 1), by {dsimp, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha} --same with tidy
}
lemma prod_all_eq_prod_two_torsion {G : Type*} [comm_group G] [fintype G]:
∏ g : G, g = ∏ g : two_torsion_subgroup G, g := -- don't need brackets
begin
have hdisj : disjoint {x : G | x ∈ two_torsion_subgroup G} {x : G | x ≠ x⁻¹ },
{
intros x hx,
cases hx with h1 h2,
norm_num,
have hA : x * x = 1, by assumption,
suffices hB : x * x ≠ 1, by exact h2 (false.rec (x = x⁻¹) (hB hA)),
clear hA h1,
simpa [← mul_eq_one_iff_eq_inv] using h2, -- simpa .. using instead of simp .. at .., assumption
},
have h : (∏ g in {x : G | x ≠ x⁻¹ }.to_finset, g) = 1,
{
apply prod_finset_distinct_inv;
finish,
},
have H : (∏ (g : G), g) = (∏ x in {x : G | x ∈ two_torsion_subgroup G}.to_finset, x)
* (∏ x in {x : G | x ≠ x⁻¹ }.to_finset, x),
{
--simp [finset.prod_union],
-- using squeeze_simp we see that simp only used one lemma here, which was ne.def
-- didn't seem like this was really changing anything so remove it!
rw ← finset.prod_union,
{
congr,
ext1,
simp only [true_iff, finset.mem_univ, set.mem_to_finset, ne.def, finset.mem_union, set.mem_set_of_eq],
rw [two_torsion_subgroup, eq_inv_iff_mul_eq_one], --neater proof
exact classical.em _,
},
{
simpa only [finset.disjoint_iff_disjoint_coe, set.coe_to_finset],
-- simp then exact (hypothesis) can be written as simpa
}
},
{
rw [H, h],
simp, -- once again simp wasnt doing much to most goals
apply finset.prod_subtype,
finish,
},
end
```

#### Johan Commelin (Jul 02 2020 at 20:45):

Probably relevant: `prod_involution`

#### Marc Masdeu (Jul 03 2020 at 10:35):

Thanks @Alex J. Best for the review! I have incorporated your suggestions, although I see no way of coming up with this

```
suffices : x⁻¹ ≠ a, from finset.mem_of_mem_insert_of_ne (h1 x (finset.mem_insert_of_mem (finset.mem_of_mem_erase h))) this,
```

on my own without spending half an hour trying different things. Would be nice if the `finish`

tactic gave something back as a hint!

@Johan Commelin : I was aware of `prod_involution`

(this is the one that wilson's theorem uses, right?), but wanted to prove the version that I needed using tactics.

Next step (we have a "summer project" with @Xavier Xarles) will be to prove that the product of all the elements of a finite elementary abelian 2-group of order > 2 is 1...

#### Jalex Stark (Jul 03 2020 at 13:54):

To expand on Johan's point, applying `prod_involution`

reduces the problem to four much easier sorries.

```
import data.fintype.card
import data.set.finite
import tactic
open_locale classical big_operators
open finset
lemma prod_finset_distinct_inv
{α : Type*} [comm_group α] {s : finset α}
(hs1 : ∀ x ∈ s, x⁻¹ ∈ s)
(hs2 : ∀ x ∈ s, x⁻¹ ≠ x)
: ∏ x in s, x = 1 :=
begin
apply @prod_involution _ _ _ _ _ (λ a ha, a⁻¹),
{ intros, rw mul_inv_self },
{ intros, apply hs2, assumption },
{ intros, simp, },
{ intros, apply hs1, assumption, },
end
```

#### Alex J. Best (Jul 07 2020 at 06:23):

Marc Masdeu said:

Would be nice if the

`finish`

tactic gave something back as a hint!

I asked about this once and was told more or less that the output would be unreadable and no quicker than just running finish again unfortunately: https://github.com/leanprover-community/mathlib/issues/1451#issuecomment-533151071

#### Marc Masdeu (Jul 10 2020 at 09:10):

Jalex Stark said:

To expand on Johan's point, applying

`prod_involution`

reduces the problem to four much easier sorries.

Thanks @Jalex Stark , we knew about this but it seemed like killing flies with cannons, so we set to prove directly what we exactly wanted. But in the long run, I agree your approach is the right one.

#### Marc Masdeu (Jul 10 2020 at 09:13):

And now I can't even start the next lemma:

```
variables {G : Type*} [comm_group G] [fintype G]
-- given G two torsion and 1 ≠ g ∈ G, there is H < G of index 2 with g ∉ H
lemma element_avoidance {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1):
∃ (H : subgroup G) , (g ∉ H ∧ (∀ x : H, x * x = 1) ∧ {x : G | x * x = 1} = H ∪ (left_coset g H)):=
begin
apply nat.case_strong_induction_on (fintype.card G),
end
```

I want to do a proof by induction on the size of G, but it complains at the first step. I can't quite make sense of the error. In trying to debug what was going on, I went for a much stupider lemma, which I can't do either!

```
lemma stupid {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1):
∃ (H : subgroup G) , H = H :=
begin
use ↑G, -- Complains!
end
```

#### Alex J. Best (Jul 10 2020 at 09:45):

One way to get `G`

as a subgroup of itself is to think of the ordering on subgroups by inclusion, `G`

is then tthe maximal, or top element, so lean understands the symbol `\top`

for `G`

as a sub of itself.

```
lemma stupid {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1):
∃ (H : subgroup G) , H = H :=
begin
use ⊤,
end
```

#### Alex J. Best (Jul 10 2020 at 09:49):

Also, be cautious using the arrow directly, if you want to coerce something try `(thing : Type)`

to tell lean which type to coerce it to, lean will print the up arrow but it can be underdetermined what you want the arrow to mean so just putting the type you want can save headaches.

#### Marc Masdeu (Jul 10 2020 at 09:50):

Yes but isn't this like cheating? I would expect that there would be some kind of coertion mechanism that would work in this case. In particular, `use (G : subgroup G)`

is more like what I'd like to work, and it doesn't. Recall that I want to really do the non-stupid lemma by induction...

#### Alex J. Best (Jul 10 2020 at 09:54):

As for your first question lean gets a bit confused because it doesn't see the cardinality of `G`

, or even `G`

really in your goal, maybe its possible to make it work, but it seems less hassle to set this up more explicitly as a statement parameterised by the caridinality of the group

```
lemma element_avoidance_aux {n : ℕ} : (fintype.card G = n) → ∀ {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1),
∃ (H : subgroup G) , (g ∉ H ∧ (∀ x : H, x * x = 1) ∧ {x : G | x * x = 1} = H ∪ (left_coset g H)):=
begin
apply nat.case_strong_induction_on n,
end
```

your original statement is then obtained as `element_avoidance_aux (rfl _)`

or something like that.

#### Alex J. Best (Jul 10 2020 at 09:59):

Marc Masdeu said:

Yes but isn't this like cheating? I would expect that there would be some kind of coertion mechanism that would work in this case. In particular,

`use (G : subgroup G)`

is more like what I'd like to work, and it doesn't. Recall that I want to really do the non-stupid lemma by induction...

I agree some automatic coercion would be nice, I'm just not sure how the setup would go. It doesn't seem to me to fit the coercion model: `G`

is a type and you can't make a coercion from any random type to `subgroup G`

, only from `G`

itself.

Top is a bit weird to look at at first, but its short to type, and you get all the lemmas about order (every subgroup is contained in top, nothing contains top, etc for free.

#### Alex J. Best (Jul 10 2020 at 10:26):

I was confused but: Ohhh I get it $H$ is index 2 only in the 2-torsion.

#### Kevin Buzzard (Jul 10 2020 at 14:01):

Coercing G into subgroup G is a dependent coercion which I don't think is possible

#### Marc Masdeu (Jul 27 2020 at 08:35):

OK so I'm Leaning again, and managed to prove the element_avoidance lemma, modulo proving the "obvious" fact that a finite subgroup has finitely many subgroups:

```
import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic
import basic
open_locale classical big_operators
variables {G : Type*} [comm_group G] [fintype G]
lemma finite_subgroups_of_finite_group : {X : subgroup G | true}.finite :=
begin
sorry
end
```

Is this something easy to do?

#### Kenny Lau (Jul 27 2020 at 08:36):

it injects to `set G`

#### Kenny Lau (Jul 27 2020 at 08:36):

also instead of that you want to say `fintype (subgroup G)`

?

#### Marc Masdeu (Jul 27 2020 at 08:37):

The exact statement that I need in my proof is this one, but maybe what you suggest is also OK?

#### Kenny Lau (Jul 27 2020 at 08:38):

```
import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic
noncomputable theory
open_locale classical big_operators
variables {G : Type*} [comm_group G] [fintype G]
instance : fintype (subgroup G) :=
fintype.of_injective (coe : subgroup G → set G) $ λ _ _, subgroup.ext'
lemma finite_subgroups_of_finite_group : {X : subgroup G | true}.finite :=
set.finite.of_fintype _
```

#### Kenny Lau (Jul 27 2020 at 08:39):

(edited)

#### Marc Masdeu (Jul 27 2020 at 08:44):

Wow!! I am trying to make sense of what just happened there... I have trouble understanding finset, fintype,... And also the `instance`

thingy. But thanks so much @Kenny Lau !

#### Marc Masdeu (Jul 27 2020 at 09:36):

After minimal cleaning, this is what I got:

```
instance : fintype (subgroup G) := fintype.of_injective (coe : subgroup G → set G) $ λ _ _, subgroup.ext'
-- given a finite group G and g ∈ G of order 2, there is H < G with g ∉ H and such that G[2] = H \cup g H.
lemma element_avoidance {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1):
∃ (H : subgroup G) ,
(g ∉ H ∧
(∀ (x : G), x ∈ H → x * x = 1) ∧
{x : G | x * x = 1} = H ∪ (left_coset g H))
:=
begin
let s := {X : subgroup G | g ∉ X ∧ (∀ x : G, x ∈ X → x*x = 1)},
have sfin : s.finite := set.finite.of_fintype _,
have snonempty : set.nonempty s,
{
use ⊥,
split,
exact h₁,
intros x hx,
rw subgroup.mem_bot at hx,
rw hx,
exact mul_one 1,
},
let existsH := set.finite.exists_maximal_wrt id s sfin snonempty,
simp only [and_imp, exists_prop, id.def, set.mem_set_of_eq] at existsH,
cases existsH with a ha,
use a,
split,
exact ha.1.1,
split,
exact ha.1.2,
-- We have defined a as the maximal subgroup of G satisfying
-- 1) g ∉ a
-- 2) ∀ x ∈ a, x*x = 1
-- Now we must show that a ∪ ga = twotorsion(G)
apply set.subset.antisymm,
{
-- Prove that twotorsion(G) ⊆ a u ga
intros x hx,
dsimp at hx,
rcases ha with ⟨ ha1, hmax ⟩ ,
cases ha1 with hga hatwotors,
by_contradiction h,
have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
let xua : subgroup G :=
{
carrier := ↑a ∪ left_coset x a,
one_mem' := or.inl (subgroup.one_mem a),
mul_mem' :=
begin
intros u v hu hv,
cases hv with hv1 hv2,
{
cases hu with hu1 hu2,
{
exact or.inl (subgroup.mul_mem a hu1 hv1),
},
{
right,
rw [mem_left_coset_iff, ←mul_assoc],
rw mem_left_coset_iff at hu2,
exact is_submonoid.mul_mem hu2 hv1,
}
},
{
cases hu with hu1 hu2,
{
right,
rw [mul_comm, mem_left_coset_iff, ←mul_assoc],
rw mem_left_coset_iff at hv2,
exact is_submonoid.mul_mem hv2 hu1,
},
{
left,
rw mem_left_coset_iff at hu2 hv2,
have H : x⁻¹ * x⁻¹ * u * v ∈ a,
{
norm_cast at hu2 hv2 ⊢,
rw [mul_comm, mul_assoc, ←mul_assoc v _, mul_comm v _],
exact subgroup.mul_mem a hv2 hu2,
},
rw [←x_eq_xinv, hx, one_mul] at H,
exact H,
},
},
end,
inv_mem' :=
begin
intros u hu,
cases hu with hu1 hu2,
{
exact or.inl (is_subgroup.inv_mem hu1),
},
{
right,
rw mem_left_coset_iff at hu2 ⊢,
norm_cast at hu2 ⊢,
rw [←subgroup.inv_mem_iff, mul_inv, inv_inv, inv_inv],
rw ←x_eq_xinv at hu2,
exact hu2,
}
end
},
have hxinxua : ∀ y : G, y ∈ xua ↔ (y ∈ ↑a ∨ y ∈ left_coset x a), by apply subgroup.mem_coe,
specialize hmax xua,
have g_notin_xua : g ∉ xua,
{
clear hmax,
by_contradiction cont,
cases cont with c1 c2,
{
solve_by_elim,
},
{
rw mem_left_coset_iff at c2,
have h2: x ∉ left_coset g ↑a,
{
rw set.mem_union_eq at h,
push_neg at h,
exact h.right,
},
rw mem_left_coset_iff at h2,
suffices h3: g⁻¹ * x ∈ ↑a, by solve_by_elim,
norm_cast at *,
rw [←subgroup.inv_mem_iff, mul_inv, mul_comm, inv_inv],
exact c2,
}
},
specialize hmax g_notin_xua,
have h_twotors : (∀ (y : G), y ∈ xua → y * y = 1),
{
intros y hy,
rw hxinxua at hy,
cases hy,
{
apply hatwotors,
exact subgroup.mem_coe.mp hy,
},
{
rw mem_left_coset_iff at hy,
have HH : ∃ w ∈ a, x⁻¹ * y = w, by tauto,
cases HH with w hw,
cases hw with hw1 hw2,
have hhy : y = x * w := eq_mul_of_inv_mul_eq hw2,
calc
y * y = (x * w) * (x * w): congr (congr_arg has_mul.mul hhy) hhy
... = (x * x) * (w * w): mul_mul_mul_comm x w x w
... = w * w : mul_left_eq_self.mpr hx
... = 1 : hatwotors w hw1,
}
},
specialize hmax h_twotors,
have htriv : a ≤ xua,
{
rw subgroup.le_def,
intros y hy,
rw hxinxua,
left,
exact hy,
},
specialize hmax htriv,
have hc : x ∈ a,
{
norm_cast at *,
rw hmax,
clear sfin snonempty s hga hatwotors h g_notin_xua htriv h_twotors h₁ h₂ hmax,
dsimp at *,
rw hxinxua,
right,
rw mem_left_coset_iff,
exact quotient_group.eq.mp rfl,
},
have hl : x ∉ a,
{
rw set.mem_union at h,
push_neg at h,
exact h.left
},
solve_by_elim,
},
{
-- prove that twotorsion(G) ⊇ a u ga
intros x hx,
by_cases (x ∈ a),
tauto,
{
have H : (x ∈ left_coset g a),
{
rw set.mem_union at hx,
tauto,
},
suffices x_is_twotors : x * x = 1, by tauto,
clear hx h,
have H2 : ∀ (x : G), x ∈ a → x * x = 1, by tauto,
rw mem_left_coset_iff at H,
specialize H2 (g⁻¹ * x) H,
have H3 : g = g⁻¹ := eq_inv_of_mul_eq_one h₂,
by calc
x * x = g * g * x * x : by simp only [h₂, one_mul]
... = g⁻¹ * g⁻¹ * x * x : by rw ← H3
... = g⁻¹ * x * g⁻¹ * x : by rw mul_right_comm g⁻¹ g⁻¹ x
... = g⁻¹ * x * (g⁻¹ * x) : by exact mul_assoc (g⁻¹ * x) g⁻¹ x
... = 1 : by exact H2,
}
},
end
```

#### Scott Morrison (Jul 27 2020 at 09:52):

Please please turn that into 10 separate lemmas. :-)

#### Marc Masdeu (Jul 27 2020 at 14:08):

Scott Morrison said:

Please please turn that into 10 separate lemmas. :-)

Have 6 so far...and done for the day :-).

```
variables {G : Type*} [comm_group G] [fintype G]
instance : fintype (subgroup G) := fintype.of_injective (coe : subgroup G → set G) $ λ _ _, subgroup.ext'
/-
If a is a subgroup of G[2] and x ∈ G[2], then a ∪ x *l a is a subgroup.
-/
def insert_twotors_to_twotors {x : G} {a : subgroup G}
(hx : x * x = 1) (ha : ∀ g : G, g ∈ a → g * g = 1) : subgroup G :=
{
carrier := ↑a ∪ left_coset x a,
one_mem' := or.inl (subgroup.one_mem a),
mul_mem' :=
begin
intros u v hu hv,
--rcases? hu hv,-- with ⟨ hu1, hu2⟩ | ⟨ hv1, hv2⟩ ,
cases hv with hv1 hv2,
repeat {cases hu with hu1 hu2},
{
exact or.inl (subgroup.mul_mem a hu1 hv1),
},
{
right,
rw [mem_left_coset_iff, ←mul_assoc],
rw mem_left_coset_iff at hu2,
exact is_submonoid.mul_mem hu2 hv1,
},
{
right,
rw [mul_comm, mem_left_coset_iff, ←mul_assoc],
rw mem_left_coset_iff at hv2,
exact is_submonoid.mul_mem hv2 hu1,
},
{
left,
rw mem_left_coset_iff at hu2 hv2,
have H : x⁻¹ * x⁻¹ * u * v ∈ a,
{
norm_cast at hu2 hv2 ⊢,
rw [mul_comm, mul_assoc, ←mul_assoc v _, mul_comm v _],
exact subgroup.mul_mem a hv2 hu2,
},
have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
rw [←x_eq_xinv, hx, one_mul] at H,
exact H,
}
end,
inv_mem' :=
begin
intros u hu,
cases hu with hu1 hu2, by exact or.inl (is_subgroup.inv_mem hu1),
{
right,
rw mem_left_coset_iff at hu2 ⊢,
norm_cast at hu2 ⊢,
rw [←subgroup.inv_mem_iff, mul_inv, inv_inv, inv_inv],
have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
rw ←x_eq_xinv at hu2,
exact hu2,
}
end
}
/--
If g ∈ G[2] and a ≤ G[2], then a ∪ g l* a ⊆ G[2].
--/
lemma twotorsion_contains_a_and_ga {g : G} {a : subgroup G}
(h₁ : g * g = 1) (h₂ : ∀ (x : G), x ∈ a → x * x = 1) :
↑a ∪ left_coset g ↑a ⊆ {x : G | x * x = 1} :=
begin
-- prove that twotorsion(G) ⊇ a u ga
intros x hx,
by_cases (x ∈ a), tauto,
have H : (x ∈ left_coset g a),
{
rw set.mem_union at hx,
norm_cast at hx,
tauto,
},
suffices x_is_twotors : x * x = 1, by tauto,
clear hx h,
have H2 : ∀ (x : G), x ∈ a → x * x = 1, by tauto,
rw mem_left_coset_iff at H,
specialize H2 (g⁻¹ * x) H,
have H3 : g = g⁻¹ := eq_inv_of_mul_eq_one h₁,
by calc
x * x = g * g * x * x : by simp only [h₁, one_mul]
... = g⁻¹ * g⁻¹ * x * x : by rw ← H3
... = g⁻¹ * x * g⁻¹ * x : by rw mul_right_comm g⁻¹ g⁻¹ x
... = g⁻¹ * x * (g⁻¹ * x) : by exact mul_assoc (g⁻¹ * x) g⁻¹ x
... = 1 : by exact H2,
end
/--
Suppose a ≤ G[2], and g ∉ a.
Then if x ∈ G[2] and x ∉ g l* a,
then g ∉ ⟨ x, a ⟩.
--/
lemma g_notin_xua {x g: G} {a : subgroup G}
(hg : g ∉ a)
(hx : x * x = 1)
(ha : ∀ y : G, y ∈ a → y * y = 1)
(hgx : x ∉ left_coset g ↑a) :
(g ∉ insert_twotors_to_twotors hx ha) :=
begin
by_contradiction cont,
cases cont,
by contradiction,
{
rw mem_left_coset_iff at *,
suffices : g⁻¹ * x ∈ ↑a, by solve_by_elim,
norm_cast at *,
rw [←subgroup.inv_mem_iff, mul_inv, mul_comm, inv_inv],
exact cont,
}
end
/--
If x ∈ G[2] and a ≤ G[2], then ⟨ x, a ⟩ ≤ G[2].
--/
lemma xua_twotors {x : G} {a : subgroup G}
(hx : x * x = 1)
(ha : ∀ y : G, y ∈ a → y * y = 1) :
(∀ (y : G), y ∈ (insert_twotors_to_twotors hx ha) → y * y = 1) :=
begin
intros y hy,
let xua := insert_twotors_to_twotors hx ha,
have hxinxua : ∀ y : G, y ∈ xua ↔ (y ∈ ↑a ∨ y ∈ left_coset x a), by apply subgroup.mem_coe,
rw hxinxua at hy,
cases hy, by exact ha y (subgroup.mem_coe.mp hy),
{
rw mem_left_coset_iff at hy,
have HH : ∃ w ∈ a, x⁻¹ * y = w, by tauto,
rcases HH with ⟨ w ,⟨ hw1, hw2⟩⟩,
have hhy : y = x * w := eq_mul_of_inv_mul_eq hw2,
calc
y * y = (x * w) * (x * w): congr (congr_arg has_mul.mul hhy) hhy
... = (x * x) * (w * w): mul_mul_mul_comm x w x w
... = w * w : mul_left_eq_self.mpr hx
... = 1 : ha w hw1,
}
end
/--
G[2] ≤ ⟨g, a⟩
--/
lemma twotorsion_containedin_a_union_ga {g : G} {a : subgroup G}
(h₁ : g * g = 1) (h₂ : ∀ (x : G), x ∈ a → x * x = 1)
(hga : g ∉ a)
(hmax : ∀ (a' : subgroup G), g ∉ a' → (∀ (x : G), x ∈ a' → x * x = 1) → a ≤ a' → a = a') :
{x : G | x * x = 1} ⊆ ↑a ∪ left_coset g ↑a :=
begin
-- Prove that twotorsion(G) ⊆ a u ga
intros x hx,
dsimp at hx,
by_contradiction h,
rw set.mem_union at h,
push_neg at h,
let xua := insert_twotors_to_twotors hx h₂,
have hxinxua : ∀ y : G, y ∈ xua ↔ (y ∈ ↑a ∨ y ∈ left_coset x a), by apply subgroup.mem_coe,
have g_notin_xua : g ∉ xua, by exact g_notin_xua hga hx h₂ h.right,
have h_twotors : (∀ (y : G), y ∈ xua → y * y = 1), by exact xua_twotors hx h₂,
have a_eq_xua : a = xua := hmax xua g_notin_xua h_twotors (λ y hy, or.inl hy),
have x_in_a : x ∈ a,
{
norm_cast at *,
rw [a_eq_xua, hxinxua, mem_left_coset_iff],
right,
simp only [subgroup.mem_coe, mul_left_inv],
exact subgroup.one_mem a
},
norm_cast at h,
have hl := h.left,
trivial,
end
-- given G two torsion and 1 ≠ g ∈ G, there is H < G of index 2 with g ∉ H
lemma element_avoidance {g : G} (h₁ : g ≠ 1) (h₂ : g * g = 1):
∃ (H : subgroup G) ,
(g ∉ H ∧
(∀ (x : G), x ∈ H → x * x = 1) ∧
{x : G | x * x = 1} = H ∪ (left_coset g H))
:=
begin
let s := {X : subgroup G | g ∉ X ∧ (∀ x : G, x ∈ X → x*x = 1)},
have sfin : s.finite := set.finite.of_fintype _,
have snonempty : set.nonempty s,
{
use ⊥,
split,
exact h₁,
intros x hx,
rw subgroup.mem_bot at hx,
rw hx,
exact mul_one 1,
},
let existsH := set.finite.exists_maximal_wrt id s sfin snonempty,
simp only [and_imp, exists_prop, id.def, set.mem_set_of_eq] at existsH,
cases existsH with a ha,
use a,
repeat {split},
exact ha.1.1,
exact ha.1.2,
-- We have defined a as the maximal subgroup of G satisfying
-- 1) g ∉ a
-- 2) ∀ x ∈ a, x*x = 1
-- Now we must show that a ∪ ga = twotorsion(G)
apply set.subset.antisymm,
apply twotorsion_containedin_a_union_ga h₂ ha.1.2 ha.1.1 ha.2,
exact twotorsion_contains_a_and_ga h₂ ha.1.2,
end
```

#### Marc Masdeu (Jul 29 2020 at 16:13):

And I still don't see the need to change the topic title... Here's another place that I've got stuck:

```
def two_torsion_subgroup (G : Type*)[comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := by simp,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
begin
tidy,
rw [mul_mul_mul_comm a b a b, ha, hb],
refine mul_one 1,
end,
inv_mem' := λ a (ha : a * a = 1), by {tidy, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha}
}
lemma two_prods_are_equal {G : Type*} [comm_group G] [fintype G]:
((∏ (g : ↥(two_torsion_subgroup G)), g) : G) = (∏ (g : G) in (two_torsion_subgroup G).carrier.to_finset, g ):=
begin
sorry
end
```

I don't manage to prove the lemma, which to me is just two different ways of writing in Lean the same exact product. I also don't see why I can't apply finset.prod_congr...

Thanks Lean community!

#### Kevin Buzzard (Jul 29 2020 at 16:30):

This is exactly the sort of thing which makes lean hard for mathematicians to use

#### Kevin Buzzard (Jul 29 2020 at 16:32):

The official answer is probably that this is #xy and you should decide once and for all how you want to talk about this subset instead of switching between different ways of talking about it

#### Kevin Buzzard (Jul 29 2020 at 16:34):

It wouldn't surprise me if you ended up with two different witnesses to finiteness of the set you're taking a product over and then nothing will work anyway and you'll have to get the forensic experts in

#### Kevin Buzzard (Jul 29 2020 at 16:35):

Did you try library_search?

#### Johan Commelin (Jul 29 2020 at 16:36):

@Marc Masdeu Sorry for the pain...

#### Johan Commelin (Jul 29 2020 at 16:36):

The reason that `finset.prod_congr`

doesn't work is because it assumes you are taking products indexed by the same type. But in your case the LHS is a subtype of the type on the right.

#### Johan Commelin (Jul 29 2020 at 16:37):

So you probably need to `rw`

the LHS using something like `finset.prod_subtype`

.

#### Kevin Buzzard (Jul 29 2020 at 16:37):

PS unrelated -- `tidy`

is only supposed to be used at the end of a proof. You might want to replace it with `tidy?`

and then with the output of what it says it's doing. It might not be doing much at all.

#### Johan Commelin (Jul 29 2020 at 16:37):

I agree that we shouldn't need to experience this pain. But I don't know how to solve it.

#### Johan Commelin (Jul 29 2020 at 16:38):

Maybe better simp-lemmas?

#### Kevin Buzzard (Jul 29 2020 at 16:50):

Delete fintype ;-)

#### Kevin Buzzard (Jul 29 2020 at 16:50):

Or at least don't tell mathematicians about it

#### Kevin Buzzard (Jul 29 2020 at 16:52):

I don't know how to solve this. We offer several ways of doing a product over a finite set and this is problematic

#### Kevin Buzzard (Jul 29 2020 at 16:53):

The problem is even more basic than this, we offer three ways to take the intersection of a bunch of sets

#### Marc Masdeu (Jul 29 2020 at 16:54):

Oh well. I understand that if I choose different ways of writing the same, then I'll have to deal with coercions and the like. I'm very surprised though that this is so hard!

I got into this because I am trying to prove some lemmas about products of elements of a finite abelian multiplicative group G. Which way should I be using? I'm happy to redo parts of what I already have.

#### Mario Carneiro (Jul 29 2020 at 16:57):

This should be generalized to a lemma about prod

#### Kevin Buzzard (Jul 29 2020 at 16:58):

The issue of course Marc is that if you only prove the result about one of them, then sooner or later someone will need it for the other variant :-)

#### Mario Carneiro (Jul 29 2020 at 16:58):

I think something like `prod (g : S), f g = prod g in T, f g`

if `S = T`

#### Mario Carneiro (Jul 29 2020 at 16:59):

where `S = T`

needs some coe or to_finset or something

#### Marc Masdeu (Jul 29 2020 at 17:00):

Here's my real problem (to avoid xy): I have proven this lemma

```
(∏ g : G, g) = (∏ g : two_torsion_subgroup G, g)
```

and this one:

```
∃ (H : subgroup G) ,
(g ∉ H ∧
(∀ (x : G), x ∈ H → x * x = 1) ∧
{x : G | x * x = 1} = H ∪ (left_coset g H))
```

The one that I'd like to prove next is:

```
lemma prod_identity {g : G} (h₁ : ∀ x : G, x * x = 1) (h₂ : g ≠ 1):
(∏ x : G, x) = g^((fintype.card G / 2) : ℕ)
```

and along the way I thought that I would easily be able to prove

```
((∏ x : two_torsion_subgroup G, x) : G) = ((∏ x : H, x) : G) * (∏ x : left_coset g ↑H, x )
```

for the subgroup H given by the previous lemma. I have already proven that the two sets (H and g *l H) are disjoint, so it seemed easy...

#### Marc Masdeu (Jul 29 2020 at 17:01):

Mario Carneiro said:

I think something like

`prod (g : S), f g = prod g in T, f g`

if`S = T`

I'll try to see if I can write a proof for this...

#### Kevin Buzzard (Jul 29 2020 at 17:04):

That looks messy and unmathematical (but important)

#### Kevin Buzzard (Jul 29 2020 at 17:06):

You look like you're on the right track but now things are going to get a bit nasty.

#### Kevin Buzzard (Jul 29 2020 at 17:08):

I've never used these finite products before but it looks to me like you're taking a product over a finite type and I think you'd be much better off taking a product over a finite subset of a type

#### Kevin Buzzard (Jul 29 2020 at 17:09):

Because then the proof that a product over H union gH equals the product over H times the product over gH will be much easier

#### Marc Masdeu (Jul 29 2020 at 17:10):

Well for me the most confusing thing is that I deal at the same time with a group and a subgroup of it, and then the product may run over subsets of either. I don't know whether I should first coerce everything as elements of the big group, and then take the corresponding set (finset?) or take the set corresponding to the element of the subgroup.

#### Johan Commelin (Jul 29 2020 at 17:14):

Kevin Buzzard said:

I've never used these finite products before but it looks to me like you're taking a product over a finite type and I think you'd be much better off taking a product over a finite subset of a type

Yup, I suggest trying to avoid the subtype

#### Kevin Buzzard (Jul 29 2020 at 17:14):

My gut feeling is that you'd be better off always working with subsets of the big group

#### Johan Commelin (Jul 29 2020 at 17:14):

(Sometimes they are useful... but most of the time I would avoid them.)

#### Marc Masdeu (Jul 29 2020 at 17:25):

I'm affraid this is not what @Mario Carneiro was asking for, right?

```
lemma two_products {α β: Type*} {s : finset α} [comm_monoid β] {t : set α} [fintype t] {f : α → β}
(h: s = t.to_finset) :
(∏ g in s, f g) = (∏ g in t.to_finset, f g) := congr_fun (congr_arg finset.prod h) (λ (g : α), f g)
```

#### Mario Carneiro (Jul 29 2020 at 17:26):

You want `t`

to be a finset

#### Mario Carneiro (Jul 29 2020 at 17:26):

and `h`

could be for example `\forall x, x \in s <-> x \in t`

#### Mario Carneiro (Jul 29 2020 at 17:27):

and `s`

should be a `set`

, with `g : s`

on the left

#### Johan Commelin (Jul 29 2020 at 17:27):

That's just `prod_congr`

, right?

#### Mario Carneiro (Jul 29 2020 at 17:27):

if you have `prod g in s`

on both sides it's just `congr`

#### Johan Commelin (Jul 29 2020 at 17:27):

Sure, but there is a lemma `prod_congr`

#### Mario Carneiro (Jul 29 2020 at 17:27):

the point here is that it's two different kinds of summations on each side

#### Mario Carneiro (Jul 29 2020 at 17:28):

`g : s`

on the left and `g in t`

on the right

#### Marc Masdeu (Jul 29 2020 at 17:28):

Oh I see. Yes, it's also confusing because the symbol is the same...If s is a finset then one can abbreviate g in s with g : s, according to what's written in big_operators.lean

#### Mario Carneiro (Jul 29 2020 at 17:28):

`prod g : s`

is really `prod (g:s) in univ`

#### Mario Carneiro (Jul 29 2020 at 17:29):

`prod g in s`

is therefore not the same (syntactically) as `prod g : s`

even if `s`

is a finset (the latter being `prod g in (univ : finset s)`

)

#### Mario Carneiro (Jul 29 2020 at 17:30):

but there should be a theorem proving they are equal

#### Marc Masdeu (Jul 29 2020 at 17:30):

OK now trying to prove this:

```
lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : set α} [fintype t] {f : α → β}
(h: ∀ x, x ∈ s ↔ x ∈ t) : (∏ g : s, f g) = (∏ g in t.to_finset, f g)
```

#### Mario Carneiro (Jul 29 2020 at 17:30):

still drop the `to_finset`

#### Mario Carneiro (Jul 29 2020 at 17:31):

`t : finset A`

#### Mario Carneiro (Jul 29 2020 at 17:31):

and no `fintype t`

assumption

#### Johan Commelin (Jul 29 2020 at 17:32):

`rw ← finset.prod_subtype, apply finset.prod_congr`

should get you moving again

#### Marc Masdeu (Jul 29 2020 at 17:35):

Not for me, @Johan Commelin ... I am trying this, as Mario suggested:

```
lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : finset α} {f : α → β}
(h: ∀ x, x ∈ s ↔ x ∈ t) : (∏ g : s, f g) = (∏ g in t, f g) :=
```

and the first rw gives me 4 goals...

#### Mario Carneiro (Jul 29 2020 at 17:37):

So now we have to start hunting through the finset and big_operator API to prove this

#### Mario Carneiro (Jul 29 2020 at 17:38):

It helps to understand what the theorem actually says, without all the nice notations. The left product is

`(finset.univ {x // x \in s}).prod (\lam x, f x.1)`

, and the right is `t.prod (\lam x : A, f x)`

#### Mario Carneiro (Jul 29 2020 at 17:40):

so you need something that talks about applying an injection (in this case `x.1`

) to change the index type

#### Mario Carneiro (Jul 29 2020 at 17:44):

I'm surprised this or something like it hasn't been proved yet. Anyway the general theorem about index changes is `prod_bij`

#### Marc Masdeu (Jul 29 2020 at 17:45):

Do mem_to_finset or coe_to_finset help? I don't know if you are trying a socratic dialogue here...

#### Mario Carneiro (Jul 29 2020 at 17:46):

You should start the proof by applying `prod_bij`

, which has a ton of assumptions that you can fill in

#### Marc Masdeu (Jul 29 2020 at 17:47):

OK, I'll try.

#### Mario Carneiro (Jul 29 2020 at 17:48):

You won't need `mem_to_finset`

and such because `to_finset`

doesn't appear in the statement anymore

#### Marc Masdeu (Jul 29 2020 at 17:52):

When I apply prod_bij, some of the goals contain a m_1. This means that it couldn't figure out what I really was applying, right?

#### Marc Masdeu (Jul 29 2020 at 17:53):

This is the first goal:

```
⊢ ∀ (a : ↥s) (ha : a ∈ finset.univ), ?m_1 a ha ∈ t
```

#### Mario Carneiro (Jul 29 2020 at 17:54):

If you use `refine prod_bij _ _ _ _ _ _ _,`

you can give the functions in the first few underscores, so that you don't get any `?m_1 a ha`

business

#### Mario Carneiro (Jul 29 2020 at 17:57):

I think the function is `\lam x _, x.1`

#### Marc Masdeu (Jul 29 2020 at 18:12):

```
lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : finset α} {f : α → β}
(h: ∀ x, x ∈ s ↔ x ∈ t) : (∏ g : s, f g) = (∏ g in t, f g) :=
begin
refine finset.prod_bij (λ x _, x.1) _ _ _ _,
{
intros a ha,
specialize h a,
apply h.mp,
exact subtype.mem a,
},
{
intros a ha,
refl,
},
{
intros a1 a2 h1 h2,
exact subtype.eq,
},
{
intros b hb,
specialize h b,
use b,
rw h,
exact hb,
split,
apply finset.mem_univ,
exact rfl,
}
end
```

#### Patrick Massot (Jul 29 2020 at 18:19):

This all sounds like issues that were obviously solved in mathcomp before formalizing the odd order theorem, but this observation is taboo here.

#### Mario Carneiro (Jul 29 2020 at 18:21):

This is a hole in the library. Of course the proof isn't nice

#### Mario Carneiro (Jul 29 2020 at 18:21):

the correct proof is to cite this theorem

#### Mario Carneiro (Jul 29 2020 at 18:21):

but the theorem didn't exist

#### Marc Masdeu (Jul 29 2020 at 18:22):

Is anyone working in improving the user experience with sets/finsets/fintypes and the like? It is basic enough that it can cause problems in many places...

#### Marc Masdeu (Jul 29 2020 at 18:23):

Patrick Massot said:

This all sounds like issues that were obviously solved in mathcomp before formalizing the odd order theorem, but this observation is taboo here.

Please elaborate, the story sounds potentially interesting!

#### Mario Carneiro (Jul 29 2020 at 18:26):

The best way to solve these problems is to have a really complete library of basic lemmas

#### Mario Carneiro (Jul 29 2020 at 18:27):

finset itself has a fairly complete API, and big_operators do too, for the most part. Like I said I'm surprised this was missed

#### Mario Carneiro (Jul 29 2020 at 18:28):

I see that `algebra.big_operators.basic`

doesn't import `fintype`

so it's impossible to state this theorem in that file. So maybe it is in another file and I missed it

#### Patrick Massot (Jul 29 2020 at 18:28):

Marc, the story is: some very smart people spend six years working on how to do finite groups in a proof assistant very close to Lean. They wrote several papers about the clever tricks they found the most useful. Sentences like "Well for me the most confusing thing is that I deal at the same time with a group and a subgroup of it," were at the heart of those papers. So we ignore them.

#### Mario Carneiro (Jul 29 2020 at 18:28):

I didn't watch closely when `algebra.big_operators`

got split into pieces

#### Mario Carneiro (Jul 29 2020 at 18:31):

eh, found it

#### Mario Carneiro (Jul 29 2020 at 18:31):

#### Patrick Massot (Jul 29 2020 at 18:32):

In the same way, there is a huge subgroup refactor going on. Those Coq people told us repeatedly that they found a very simple criterion to see whether we get this right: painlessly state and prove the third isomorphism theorem. So we invest a lot of time in the refactor and never discuss how this test will go once the refactor will be done (I asked the question several time and never got any answer).

#### Marc Masdeu (Jul 29 2020 at 18:41):

Do you think that the 3rd iso theorem will go bad after this, then??

#### Kevin Buzzard (Jul 29 2020 at 18:44):

Patrick, my impression in the odd order work is that they solve this by never talking about the cardinality of a type. Every group is a subgroup of a large ambient group and they only have one notion of cardinality, that of a subset of a group.

As for refactoring subgroups, I think that the third isomorphism theorem should be easy with bundled subgroups but I can't check until Friday. We have a really nice `map`

and `comap`

for group homs. We have N and K normal in G and N a subset of K, we have a construction making a subgroup a group. I don't envisage any problems

#### Mario Carneiro (Jul 29 2020 at 19:23):

Here's the statement

```
import group_theory.quotient_group data.equiv.mul_add
variables {α : Type*} [group α]
def image_normal {G H} [group G] [group H]
(f : G → H) [is_group_hom f] (hf : function.surjective f)
(s : set G) [normal_subgroup s] : normal_subgroup (f '' s) :=
⟨begin
rintro _ ⟨a, h, rfl⟩ b,
obtain ⟨b, rfl⟩ := hf b,
refine ⟨_, normal_subgroup.normal a h b, _⟩,
rw [is_mul_hom.map_mul f, is_mul_hom.map_mul f, is_group_hom.map_inv f],
end⟩
structure normal_subgroup' (α) [group α] :=
(carrier : set α) [is_normal : normal_subgroup carrier]
attribute [instance] normal_subgroup'.is_normal
def to_subgroup (s : normal_subgroup' α) : subgroup α := subgroup.of s.carrier
instance normal_subgroup'.coe_subgroup : has_coe (normal_subgroup' α) (subgroup α) := ⟨to_subgroup⟩
instance normal_subgroup'.coe_normal_subgroup (s : normal_subgroup' α) :
normal_subgroup (s : set α) := normal_subgroup'.is_normal _
instance normal_subgroup'.coe_coe_normal_subgroup (s : normal_subgroup' α) :
normal_subgroup ((s : subgroup α) : set α) := normal_subgroup'.is_normal _
instance : preorder (normal_subgroup' α) := preorder.lift normal_subgroup'.carrier
def normal_subgroup'.image {G H} [group G] [group H] (f : G →* H) (hf : function.surjective f)
(s : normal_subgroup' G) : normal_subgroup' H :=
by haveI := image_normal f hf s; exact ⟨f '' s⟩
namespace quotient_group
def quotient' [group α] (s : normal_subgroup' α) : Type* := quotient ((s : subgroup α) : set α)
variables [group α] {s : normal_subgroup' α}
instance quotient_group.group' (s : normal_subgroup' α) : group (quotient' s) :=
quotient_group.group s
def mk' : α → quotient' s := quotient.mk'
instance mk'.is_group_hom : is_group_hom (mk' : α → quotient' s) := quotient_group.is_group_hom _
def mk_hom : α →* quotient' s := monoid_hom.of mk'
variable (s)
def below (t : normal_subgroup' α) : normal_subgroup' (quotient' s) :=
t.image mk_hom $ by rintro ⟨i⟩; exact ⟨_, rfl⟩
end quotient_group
theorem third_isomorphism_thm {G} [group G] {H K : normal_subgroup' G} (h : H ≤ K) :
quotient_group.quotient' (quotient_group.below H K) ≃* quotient_group.quotient' H :=
sorry
```

#### Mario Carneiro (Jul 29 2020 at 19:25):

the proof is easier if you have all the hom functions doing equalizer tricks

#### Kevin Buzzard (Jul 29 2020 at 20:11):

is_group_hom is deprecated

#### Mario Carneiro (Jul 29 2020 at 20:20):

I know?

#### Mario Carneiro (Jul 29 2020 at 20:20):

For the purpose of simplifying the proof, I'm using the deprecated lemmas to prove the bundled ones. In a proper refactor you would rewrite the proofs

#### Mario Carneiro (Jul 29 2020 at 20:22):

The hard part here, as ever, is just setting up statements - ignore the proofs, which are all trivial anyway

#### Mario Carneiro (Jul 29 2020 at 20:22):

I only had to prove one theorem about `is_group_hom`

which was missing from the library (`image_normal`

)

#### Kevin Buzzard (Jul 29 2020 at 20:30):

In the bundling subgroup refactor we still don't bundle normal subgroups. I don't know what I feel about this. In the group theory game we're going to bundle them

#### Mario Carneiro (Jul 29 2020 at 20:32):

I know, I wondered about this as well. I think there is a good argument for bundling them - `quotient`

is naturally a function on it, and the whole family `ker`

/`im`

/`map`

/`comap`

/ complete lattice structure exists for them

#### Mario Carneiro (Jul 29 2020 at 20:33):

the downside is that now we have a more complicated coercion graph

#### Marc Masdeu (Jul 30 2020 at 10:46):

OK, back to finsets... Here's a puzzle which doesn't involve unions and the such:

```
variables {G : Type*} [comm_group G] [fintype G]
lemma fintype_card_eq_finset_card' : fintype.card G =
finset.card (((⊤ : subgroup G) : set G).to_finset):=
begin
sorry
end
```

#### Kenny Lau (Jul 30 2020 at 10:49):

```
import data.fintype.card group_theory.subgroup
variables {G : Type*} [comm_group G] [fintype G]
open_locale classical
lemma fintype_card_eq_finset_card' :
fintype.card G = finset.card (((⊤ : subgroup G) : set G).to_finset):=
begin
unfold fintype.card, congr, rw subgroup.coe_top, convert set.to_finset_univ.symm,
end
```

#### Kenny Lau (Jul 30 2020 at 10:49):

we need @Kevin Buzzard 's `fincard`

#### Marc Masdeu (Jul 30 2020 at 10:55):

Thanks for teaching me the `convert`

tactic, @Kenny Lau !

#### Kenny Lau (Jul 30 2020 at 10:55):

cheers

#### Kevin Buzzard (Jul 30 2020 at 11:15):

I don't know if I pushed it to the group theory game repo. If I didn't then it's inaccessible until Friday evening

#### Marc Masdeu (Jul 31 2020 at 14:29):

Thanks to @Johan Commelin, @Kenny Lau , @Kevin Buzzard, @Mario Carneiro (and probably others that on Zulip that I am forgetting) I have managed to formalize (the proof of) a non-trivial group-theory statement:

```
theorem prod_identity_general {G : Type*} [comm_group G] [fintype G] {g : G} (h1 : g ≠ 1) (h2 : g * g = 1) :
(∏ x : G, x) = g^(fintype.card (two_torsion_subgroup G) / 2)
```

I'll try next to apply it to (Z/nZ)^*...

#### Carl Friedrich Bolz-Tereick (Aug 01 2020 at 01:26):

Awesome! Is your code online somewhere?

Last updated: May 16 2021 at 05:21 UTC