Frustration with finset

Stream: new members

[Marc Masdeu]

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]

congr, ext, simp

[Johan Commelin]

@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]

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]

Ok, no worries!

[Marc Masdeu]

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]

apply finset.prod_congr --?

[Marc Masdeu]

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]

Aah, of course

[Johan Commelin]

The rhs is over some subgroup.

[Johan Commelin]

rw finset.prod_subtype?

[Johan Commelin]

If all else fails, there is finset.prod_bij but I would try to avoid that.

[Marc Masdeu]

finset.prod_subtype does not seem to exists...

[Johan Commelin]

import data.fintype.card? I think

[Marc Masdeu]

This has worked:

    rw finset.prod_subtype,
    tauto,
    finish,

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

[Mario Carneiro]

prod_subtype is missing

[Mario Carneiro]

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]

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]

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]

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]

Probably relevant: prod_involution

[Marc Masdeu]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Marc Masdeu]

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]

it injects to set G

[Kenny Lau]

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

[Marc Masdeu]

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

[Kenny Lau]

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]

(edited)

[Marc Masdeu]

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]

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]

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

[Marc Masdeu]

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]

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]

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

[Kevin Buzzard]

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]

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]

Did you try library_search?

[Johan Commelin]

@Marc Masdeu Sorry for the pain...

[Johan Commelin]

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]

So you probably need to rw the LHS using something like finset.prod_subtype.

[Kevin Buzzard]

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]

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

[Johan Commelin]

Maybe better simp-lemmas?

[Kevin Buzzard]

Delete fintype ;-)

[Kevin Buzzard]

Or at least don't tell mathematicians about it

[Kevin Buzzard]

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]

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

[Marc Masdeu]

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]

This should be generalized to a lemma about prod

[Kevin Buzzard]

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]

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

[Mario Carneiro]

where S = T needs some coe or to_finset or something

[Marc Masdeu]

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]

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]

That looks messy and unmathematical (but important)

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Marc Masdeu]

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]

You want t to be a finset

[Mario Carneiro]

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

[Mario Carneiro]

and s should be a set, with g : s on the left

[Johan Commelin]

That's just prod_congr, right?

[Mario Carneiro]

if you have prod g in s on both sides it's just congr

[Johan Commelin]

Sure, but there is a lemma prod_congr

[Mario Carneiro]

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

[Mario Carneiro]

g : s on the left and g in t on the right

[Marc Masdeu]

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]

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

[Mario Carneiro]

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]

but there should be a theorem proving they are equal

[Marc Masdeu]

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]

still drop the to_finset

[Mario Carneiro]

t : finset A

[Mario Carneiro]

and no fintype t assumption

[Johan Commelin]

rw ← finset.prod_subtype, apply finset.prod_congr should get you moving again

[Marc Masdeu]

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]

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

[Mario Carneiro]

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]

so you need something that talks about applying an injection (in this case x.1) to change the index type

[Mario Carneiro]

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]

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

[Mario Carneiro]

You should start the proof by applying prod_bij, which has a ton of assumptions that you can fill in

[Marc Masdeu]

OK, I'll try.

[Mario Carneiro]

You won't need mem_to_finset and such because to_finset doesn't appear in the statement anymore

[Marc Masdeu]

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]

This is the first goal:

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

[Mario Carneiro]

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]

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

[Marc Masdeu]

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]

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]

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

[Mario Carneiro]

the correct proof is to cite this theorem

[Mario Carneiro]

but the theorem didn't exist

[Marc Masdeu]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

I didn't watch closely when algebra.big_operators got split into pieces

[Mario Carneiro]

eh, found it

[Mario Carneiro]

src#finset.prod_subtype

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

is_group_hom is deprecated

[Mario Carneiro]

I know?

[Mario Carneiro]

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]

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

[Mario Carneiro]

I only had to prove one theorem about is_group_hom which was missing from the library (image_normal)

[Kevin Buzzard]

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]

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]

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

[Marc Masdeu]

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]

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]

we need @Kevin Buzzard 's fincard

[Marc Masdeu]

Thanks for teaching me the convert tactic, @Kenny Lau !

[Kenny Lau]

cheers

[Kevin Buzzard]

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]

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]

Awesome! Is your code online somewhere?