Finset, Set, Subgroup, Fintype

Stream: new members

[Nick_adfor]

I have questions about Finset, Set, Subgroup, Fintype in my code, and I cannot continue writing now.

import Mathlib

open Equiv Perm

def doubleTranspositions : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 2 3,
   swap 0 2 * swap 1 3,
   swap 0 3 * swap 1 2]

lemma doubleTranspositions_mem_A4 :
    ∀ σ ∈ doubleTranspositions, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

def ThreeCycles : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 0 2,  -- (0 1 2)
   swap 0 2 * swap 0 1,  -- (0 2 1)
   swap 0 1 * swap 0 3,  -- (0 1 3)
   swap 0 3 * swap 0 1,  -- (0 3 1)
   swap 0 2 * swap 0 3,  -- (0 2 3)
   swap 0 3 * swap 0 2,  -- (0 3 2)
   swap 1 2 * swap 1 3,  -- (1 2 3)
   swap 1 3 * swap 1 2]  -- (1 3 2)
--lean does not have a good way to deFine a list of all 3-cycles, so I use swap products.

lemma ThreeCycles_mem_A4 :
    ∀ σ ∈ ThreeCycles, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

lemma one_mem_A4 : (1 : Perm (Fin 4)) ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Perm.sign_one]

def generators : List (Perm (Fin 4)) :=
  (1 : Perm (Fin 4)) :: (ThreeCycles ++ doubleTranspositions)

def G : Subgroup (Perm (Fin 4)) := Subgroup.closure generators.toFinset

def set_of_generators := generators.toFinset

noncomputable instance fintypeG : Fintype ↥G := by
  exact Fintype.ofFinite ↥G

noncomputable instance fintypeG.carrier : Fintype G.carrier := by
  exact Fintype.ofFinite G

lemma gens_subset_G : set_of_generators.toSet ⊆ G.carrier := Subgroup.subset_closure

@[simp] lemma coe_fintypeCard {s : Set α} [Fintype s] : Fintype.card s = s.encard := by
  simp [Set.encard_eq_coe_toFinset_card]

lemma gens_smaller_G : set_of_generators.card ≤ Fintype.card G.carrier := by
  apply ENat.coe_le_coe.mp
  rw [coe_fintypeCard, Set.encard_eq_coe_toFinset_card]
  apply ENat.coe_le_coe.mpr
  apply Finset.card_le_card
  simp [gens_subset_G]

theorem G_eq_A4 : G = alternatingGroup (Fin 4) := by
  -- Step 2: Therefore, the cardinality of the generators set is less than or equal to the cardinality of G
  have h1 : set_of_generators.card ≤ Fintype.card ↥G := by
    exact gens_smaller_G
  -- Step 3: From the lemma `G_subgroup_A4`, we know G is a subgroup of A₄, so card G ≤ card A₄
  have h2 : Fintype.card G ≤ Fintype.card (alternatingGroup (Fin 4)) := by
    sorry
......

Now I cannot solve the sorry.