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