cosset

Stream: mathlib4

[vxctyxeha]

Can this code be simplified?

import Mathlib
open Equiv Equiv.Perm Subgroup Set Finset MulOpposite
open Classical
open scoped Pointwise
abbrev S3 := Perm (Fin 3)
theorem H_left_cosets_in_S3_local_defs :
    let H : Subgroup S3 := Subgroup.closure {swap 0 1}
    let S3_elements : Finset S3 := univ
    Finset.image (fun g => g • (H : Set S3)) S3_elements =
    {
      {1, swap 0 1},                      -- H = eH
      {swap 0 2, swap 0 1 * swap 1 2},    -- (0 2)H = {(0 2), (0 1 2)}
      {swap 1 2, swap 1 2 * swap 0 1}     -- (1 2)H = {(1 2), (0 2 1)}
    }
  := by
    sorry
theorem H_right_cosets_in_S3_local_defs :
    let H : Subgroup S3 := Subgroup.closure {swap 0 1}
    let S3_elements : Finset S3 := univ
    Finset.image (fun g => op g • (H : Set S3)) S3_elements =

    {
      {1, swap 0 1},                     -- H = He
      {swap 0 2, swap 1 2 * swap 0 1},    -- H(0 2) = {(0 2), (0 2 1)}
      {swap 1 2, swap 0 1 * swap 1 2}     -- H(1 2) = {(1 2), (0 1 2)}
    }
  := by
    sorry

[Kim Morrison]

State it as two separate theorems.

[Edison Xie]

import Mathlib

open scoped Pointwise
abbrev S3 := Equiv.Perm (Fin 3)

open Equiv MulOpposite in
theorem h (H : Subgroup S3) (hH : H = Subgroup.closure {swap 0 1}) :
    {g • (H : Set S3) | g : S3} = {{1, swap 0 1}, {swap 0 2, swap 0 1 * swap 1 2},
    {swap 1 2, swap 1 2 * swap 0 1}} ∧ {op g • (H : Set S3) | g : S3} = {{1, swap 0 1},
    {swap 0 2, swap 1 2 * swap 0 1}, {swap 1 2, swap 0 1 * swap 1 2}} := by
  sorry

[vxctyxeha]

What does it represent? too many arguments supplied to use

import Mathlib
open Function Nat Pointwise

abbrev S3 := Equiv.Perm (Fin 3)
open Equiv MulOpposite
theorem Subgroup.index_op {G : Type*} [Group G] (H : Subgroup G) :
    H.op.index = H.index := by
  trans (H.comap (MulEquiv.inv' G).symm.toMonoidHom).index
  · congr 1
    ext; simp
  · exact Subgroup.index_comap_of_surjective _ (MulEquiv.inv' G).symm.surjective
theorem h (H : Subgroup S3) (hH : H = Subgroup.closure {swap 0 1}) :
    {g • (H : Set S3) | g : S3} = {{1, swap 0 1}, {swap 0 2, swap 0 1 * swap 1 2},
    {swap 1 2, swap 1 2 * swap 0 1}} ∧ {op g • (H : Set S3) | g : S3} = {{1, swap 0 1},
    {swap 0 2, swap 1 2 * swap 0 1}, {swap 1 2, swap 0 1 * swap 1 2}} := by
  let e : S3 := 1
  let s01 : S3 := Equiv.swap 0 1
  let s02 : S3 := Equiv.swap 0 2
  let s12 : S3 := Equiv.swap 1 2
  let c012 : S3 := s01 * s12 -- (01)(12) = (012)
  let c021 : S3 := s12 * s01 -- (12)(01) = (021)
  have H_set_eq : (H : Set S3) = {e, s01} := by
    rw [hH] -- Substitute the definition of H
    ext x
    rw [SetLike.mem_coe, Subgroup.mem_closure_singleton]
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
    constructor
    rintro ⟨k, rfl⟩ -- Assume x = s01 ^ k
    have h_s01_sq : s01 ^ 2 = e := by native_decide
    have h_order_s01_is_2 : orderOf s01 = 2 := by
        rw [@orderOf_eq_prime_iff];apply And.intro;rw [h_s01_sq] ;simp only [ne_eq, s01, e]
        decide -- 展开定义，目标变为 Equiv.swap (0 : Fin 3) 1 ≠ 1
    rw [← zpow_mod_orderOf s01 k, h_order_s01_is_2]
    rcases Int.emod_two_eq_zero_or_one k with h_mod_eq_zero | h_mod_eq_one
    left;simp only [cast_ofNat, s01];rw [h_mod_eq_zero];simp;rfl
    right;simp only [cast_ofNat, s01];rw [h_mod_eq_one];simp
    --Mathlib, this might be Subgroup.mem_closure_singleton)
    rintro (rfl | rfl) -- Case on x = e or x = s01
    use 0; simp -- If x = e, use k = 0, s01 ^ 0 = e
    use 1; simp -- If x = s01, use k = 1, s01 ^ 1 = s01