/-
Copyright (c) 2015 Haitao Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author : Haitao Zhang
-/

-- develop the concept of finite subgroups based on finsets so that the properties
-- can be used directly without translating from the set based theory first

import data algebra.group .subgroup
open function finset
-- ⁻¹ in eq.ops conflicts with group ⁻¹
open eq.ops

namespace group_theory
open ops

section subg
-- we should be able to prove properties using finsets directly
variables {G : Type} [group G]

definition finset_mul_closed_on [reducible] (H : finset G) : Prop :=
           ∀ x y : G, x ∈ H → y ∈ H → x * y ∈ H
definition finset_has_inv (H : finset G) : Prop :=
           ∀ a : G, a ∈ H → a⁻¹ ∈ H

structure is_finsubg [class] (H : finset G) : Type :=
          (has_one : 1 ∈ H)
          (mul_closed : finset_mul_closed_on H)
          (has_inv : finset_has_inv H)

definition univ_is_finsubg [instance] [finG : fintype G] : is_finsubg (@finset.univ G _) :=
is_finsubg.mk !mem_univ (λ x y Px Py, !mem_univ) (λ a Pa, !mem_univ)

definition one_is_finsubg [instance] : is_finsubg (singleton (1:G)) :=
is_finsubg.mk !mem_singleton
  (λ x y Px Py, by rewrite [eq_of_mem_singleton Px, eq_of_mem_singleton Py, one_mul]; apply mem_singleton)
  (λ x Px, by rewrite [eq_of_mem_singleton Px, one_inv]; apply mem_singleton)

lemma finsubg_has_one (H : finset G) [h : is_finsubg H] : 1 ∈ H :=
      @is_finsubg.has_one G _ H h
lemma finsubg_mul_closed (H : finset G) [h : is_finsubg H] {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
      @is_finsubg.mul_closed G _ H h x y
lemma finsubg_has_inv (H : finset G) [h : is_finsubg H] {a : G} :  a ∈ H → a⁻¹ ∈ H :=
      @is_finsubg.has_inv G _ H h a

variable [decidable_eq G]

definition finsubg_to_subg [instance] {H : finset G} [h : is_finsubg H]
         : is_subgroup (ts H) :=
           is_subgroup.mk
           (mem_eq_mem_to_set H 1 ▸ finsubg_has_one H)
           (take x y, begin repeat rewrite -mem_eq_mem_to_set,
             apply finsubg_mul_closed H end)
           (take a, begin repeat rewrite -mem_eq_mem_to_set,
             apply finsubg_has_inv H end)

open nat
lemma finsubg_eq_singleton_one_of_card_one {H : finset G} [h : is_finsubg H] :
  card H = 1 → H = singleton 1 :=
assume Pcard, eq.symm (eq_of_card_eq_of_subset (by rewrite [Pcard])
  (subset_of_forall take g,
    by rewrite [mem_singleton_eq]; intro Pg; rewrite Pg; exact finsubg_has_one H))

end subg

section fin_lcoset

open set

variables {A : Type} [decidable_eq A] [group A]

definition fin_lcoset (H : finset A) (a : A) := finset.image (lmul_by a) H

definition fin_rcoset (H : finset A) (a : A) : finset A := image (rmul_by a) H

definition fin_lcosets (H G : finset A) := image (fin_lcoset H) G

definition fin_inv : finset A → finset A := image inv

variable {H : finset A}

lemma lmul_rmul {a b : A} : (lmul_by a) ∘ (rmul_by b) = (rmul_by b) ∘ (lmul_by a) :=
funext take c, calc a*(c*b) = (a*c)*b : mul.assoc

lemma fin_lrcoset_comm {a b : A} :
  fin_lcoset (fin_rcoset H b) a = fin_rcoset (fin_lcoset H a) b :=
by esimp [fin_lcoset, fin_rcoset]; rewrite [-*image_compose, lmul_rmul]

lemma inv_mem_fin_inv {a : A} : a ∈ H → a⁻¹ ∈ fin_inv H :=
assume Pin, mem_image Pin rfl

lemma fin_lcoset_eq (a : A) : ts (fin_lcoset H a) = a ∘> (ts H) := calc
      ts (fin_lcoset H a) = coset.l a (ts H) : to_set_image
      ... = a ∘> (ts H) : glcoset_eq_lcoset

lemma fin_lcoset_id : fin_lcoset H 1 = H :=
by rewrite [eq_eq_to_set_eq, fin_lcoset_eq, glcoset_id]

lemma fin_lcoset_compose (a b : A) : fin_lcoset (fin_lcoset H b) a = fin_lcoset H (a*b) :=
to_set.inj (by rewrite [*fin_lcoset_eq, glcoset_compose])

lemma fin_lcoset_inv (a : A) : fin_lcoset (fin_lcoset H a) a⁻¹ = H :=
to_set.inj (by rewrite [*fin_lcoset_eq, glcoset_inv])

lemma fin_lcoset_card (a : A) : card (fin_lcoset H a) = card H :=
      card_image_eq_of_inj_on (lmul_inj_on a (ts H))
lemma fin_lcosets_card_eq {G : finset A} : ∀ gH, gH ∈ fin_lcosets H G → card gH = card H :=
      take gH, assume Pcosets, obtain g Pg, from exists_of_mem_image Pcosets,
      and.right Pg ▸ fin_lcoset_card g

variable [is_finsubgH : is_finsubg H]
include is_finsubgH

lemma fin_lcoset_same (x a : A) : x ∈ (fin_lcoset H a) = (fin_lcoset H x = fin_lcoset H a) :=
      begin
        rewrite mem_eq_mem_to_set,
        rewrite [eq_eq_to_set_eq, *(fin_lcoset_eq x), fin_lcoset_eq a],
        exact (subg_lcoset_same x a)
      end
lemma fin_mem_lcoset (g : A) : g ∈ fin_lcoset H g :=
      have P : g ∈ g ∘> ts H, from and.left (subg_in_coset_refl g),
      assert P1 : g ∈ ts (fin_lcoset H g), from eq.symm (fin_lcoset_eq g) ▸ P,
      eq.symm (mem_eq_mem_to_set _ g) ▸ P1
lemma fin_lcoset_subset {S : finset A} (Psub : S ⊆ H) : ∀ x, x ∈ H → fin_lcoset S x ⊆ H :=
      assert Psubs : set.subset (ts S) (ts H), from subset_eq_to_set_subset S H ▸ Psub,
      take x, assume Pxs : x ∈ ts H,
      assert Pcoset : set.subset (x ∘> ts S) (ts H), from subg_lcoset_subset_subg Psubs x Pxs,
      by rewrite [subset_eq_to_set_subset, fin_lcoset_eq x]; exact Pcoset

lemma finsubg_lcoset_id {a : A} : a ∈ H → fin_lcoset H a = H :=
by rewrite [eq_eq_to_set_eq, fin_lcoset_eq, mem_eq_mem_to_set]; apply subgroup_lcoset_id

lemma finsubg_inv_lcoset_eq_rcoset {a : A} :
  fin_inv (fin_lcoset H a) = fin_rcoset H a⁻¹ :=
begin
  esimp [fin_inv, fin_lcoset, fin_rcoset],
  rewrite [-image_compose],
  apply ext, intro b,
  rewrite [*mem_image_iff, ↑compose, ↑lmul_by, ↑rmul_by],
  apply iff.intro,
    intro Pl, cases Pl with h Ph, cases Ph with Pin Peq,
    existsi h⁻¹, apply and.intro,
      exact finsubg_has_inv H Pin,
      rewrite [-mul_inv, Peq],
    intro Pr, cases Pr with h Ph, cases Ph with Pin Peq,
    existsi h⁻¹, apply and.intro,
      exact finsubg_has_inv H Pin,
      rewrite [mul_inv, inv_inv, Peq],
end

lemma finsubg_conj_closed {g h : A} : g ∈ H → h ∈ H → g ∘c h ∈ H :=
assume Pgin Phin, finsubg_mul_closed H (finsubg_mul_closed H Pgin Phin) (finsubg_has_inv H Pgin)

variable {G : finset A}
variable [is_finsubgG : is_finsubg G]
include is_finsubgG

open finset.partition

definition fin_lcoset_partition_subg (Psub : H ⊆ G) :=
      partition.mk G (fin_lcoset H) fin_lcoset_same
        (restriction_imp_union (fin_lcoset H) fin_lcoset_same (fin_lcoset_subset Psub))

open nat

theorem lagrange_theorem (Psub : H ⊆ G) : card G = card (fin_lcosets H G) * card H := calc
        card G = finset.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub)
        ... = finset.Sum (fin_lcosets H G) (λ x, card H) : finset.Sum_ext (take g P, fin_lcosets_card_eq g P)
        ... = card (fin_lcosets H G) * card H : Sum_const_eq_card_mul

end fin_lcoset

section
open fintype list subtype

lemma dinj_tag {A : Type} (P : A → Prop) : dinj P tag :=
take a₁ a₂ Pa₁ Pa₂ Pteq, subtype.no_confusion Pteq (λ Pe Pqe, Pe)

open nat

lemma card_pos {A : Type} [ambientA : group A] [finA : fintype A] : 0 < card A :=
  length_pos_of_mem (mem_univ 1)

end

section lcoset_fintype
open fintype list subtype

variables {A : Type} [group A] [fintype A] [decidable_eq A]

variables G H : finset A

definition is_fin_lcoset [reducible] (S : finset A) : Prop :=
  ∃ g, g ∈ G ∧ fin_lcoset H g = S

definition to_list : list A := list.filter (λ g, g ∈ G) (elems A)

definition list_lcosets : list (finset A) := erase_dup (map (fin_lcoset H) (to_list G))

definition lcoset_type [reducible] : Type := {S : finset A | is_fin_lcoset G H S}

definition all_lcosets : list (lcoset_type G H) :=
dmap (is_fin_lcoset G H) tag (list_lcosets G H)

variables {G H} [finsubgG : is_finsubg G]

include finsubgG

lemma self_is_lcoset : is_fin_lcoset G H H :=
exists.intro 1 (and.intro !finsubg_has_one fin_lcoset_id)

lemma lcoset_subset_of_subset (J : lcoset_type G H) : H ⊆ G → elt_of J ⊆ G :=
assume Psub, obtain j Pjin Pj, from has_property J,
by rewrite [-Pj]; apply fin_lcoset_subset Psub; exact Pjin

variables (G H)

definition lcoset_one : lcoset_type G H := tag H self_is_lcoset

variables {G H}

definition lcoset_lmul {g : A} (Pgin : g ∈ G) (S : lcoset_type G H)
  : lcoset_type G H :=
tag (fin_lcoset (elt_of S) g)
  (obtain f Pfin Pf, from has_property S,
  exists.intro (g*f)
    (by apply and.intro;
      exact finsubg_mul_closed G Pgin Pfin;
      rewrite [-Pf, -fin_lcoset_compose]))

definition lcoset_mul (S₁ S₂ : lcoset_type G H): finset A :=
Union (elt_of S₁) (fin_lcoset (elt_of S₂))

lemma mul_mem_lcoset_mul (J K : lcoset_type G H) {g h} :
  g ∈ elt_of J → h ∈ elt_of K → g*h ∈ lcoset_mul J K :=
assume Pg, begin
  rewrite [↑lcoset_mul, mem_Union_iff, ↑fin_lcoset],
  intro Ph, existsi g, apply and.intro, exact Pg,
  rewrite [mem_image_iff, ↑lmul_by],
  existsi h, exact and.intro Ph rfl
end

lemma is_lcoset_of_mem_list_lcosets {S : finset A}
  : S ∈ list_lcosets G H → is_fin_lcoset G H S :=
assume Pin, obtain g Pgin Pg, from exists_of_mem_map (mem_of_mem_erase_dup Pin),
exists.intro g (and.intro (of_mem_filter Pgin) Pg)

lemma mem_list_lcosets_of_is_lcoset {S : finset A}
  : is_fin_lcoset G H S → S ∈ list_lcosets G H :=
assume Plcoset, obtain g Pgin Pg, from Plcoset,
Pg ▸ mem_erase_dup (mem_map _ (mem_filter_of_mem (complete g) Pgin))

lemma fin_lcosets_eq :
  fin_lcosets H G = to_finset_of_nodup (list_lcosets G H) !nodup_erase_dup :=
ext (take S, iff.intro
  (λ Pimg, mem_list_lcosets_of_is_lcoset (exists_of_mem_image Pimg))
  (λ Pl, obtain g Pg, from is_lcoset_of_mem_list_lcosets Pl,
    iff.elim_right !mem_image_iff (is_lcoset_of_mem_list_lcosets Pl)))

lemma length_all_lcosets : length (all_lcosets G H) = card (fin_lcosets H G) :=
eq.trans
  (show length (all_lcosets G H) = length (list_lcosets G H), from
    assert Pmap : map elt_of (all_lcosets G H) = list_lcosets G H, from
      map_dmap_of_inv_of_pos (λ S P, rfl) (λ S, is_lcoset_of_mem_list_lcosets),
    by rewrite[-Pmap, length_map])
  (by rewrite fin_lcosets_eq)

lemma lcoset_lmul_compose {f g : A} (Pf : f ∈ G) (Pg : g ∈ G) (S : lcoset_type G H) :
lcoset_lmul Pf (lcoset_lmul Pg S) = lcoset_lmul (finsubg_mul_closed G Pf Pg) S :=
subtype.eq !fin_lcoset_compose

lemma lcoset_lmul_one (S : lcoset_type G H) : lcoset_lmul !finsubg_has_one S = S :=
subtype.eq fin_lcoset_id

lemma lcoset_lmul_inv {g : A} {Pg : g ∈ G} (S : lcoset_type G H) :
  lcoset_lmul (finsubg_has_inv G Pg) (lcoset_lmul Pg S) = S :=
subtype.eq (to_set.inj begin
 esimp [lcoset_lmul],
 rewrite [fin_lcoset_compose, mul.left_inv, fin_lcoset_eq, glcoset_id]
end)

lemma lcoset_lmul_inj {g : A} {Pg : g ∈ G}:
  @injective (lcoset_type G H) _ (lcoset_lmul Pg) :=
injective_of_has_left_inverse (exists.intro (lcoset_lmul (finsubg_has_inv G Pg)) lcoset_lmul_inv)

lemma card_elt_of_lcoset_type (S : lcoset_type G H) : card (elt_of S) = card H :=
obtain f Pfin Pf, from has_property S, Pf ▸ fin_lcoset_card f

definition lcoset_fintype [instance] : fintype (lcoset_type G H) :=
fintype.mk (all_lcosets G H)
  (dmap_nodup_of_dinj (dinj_tag (is_fin_lcoset G H)) !nodup_erase_dup)
  (take s, subtype.destruct s (take S, assume PS, mem_dmap PS (mem_list_lcosets_of_is_lcoset PS)))

lemma card_lcoset_type : card (lcoset_type G H) = card (fin_lcosets H G) :=
length_all_lcosets

open nat
variable [finsubgH : is_finsubg H]
include finsubgH

theorem lagrange_theorem' (Psub : H ⊆ G) : card G = card (lcoset_type G H) * card H :=
calc card G = card (fin_lcosets H G) * card H : lagrange_theorem Psub
        ... = card (lcoset_type G H) * card H : card_lcoset_type

lemma lcoset_disjoint {S₁ S₂ : lcoset_type G H} : S₁ ≠ S₂ → elt_of S₁ ∩ elt_of S₂ = ∅ :=
obtain f₁ Pfin₁ Pf₁, from has_property S₁,
obtain f₂ Pfin₂ Pf₂, from has_property S₂,
assume Pne, inter_eq_empty_of_disjoint (disjoint.intro
  take g, begin
  rewrite [-Pf₁, -Pf₂, *fin_lcoset_same],
  intro Pgf₁, rewrite [Pgf₁, Pf₁, Pf₂],
  intro Peq, exact absurd (subtype.eq Peq) Pne
  end )

lemma card_Union_lcosets (lcs : finset (lcoset_type G H)) :
  card (Union lcs elt_of) = card lcs * card H :=
calc card (Union lcs elt_of) = ∑ lc ∈ lcs, card (elt_of lc) : card_Union_of_disjoint lcs elt_of (λ (S₁ S₂ : lcoset_type G H) P₁ P₂ Pne, lcoset_disjoint Pne)
                         ... = ∑ lc ∈ lcs, card H : Sum_ext (take lc P, card_elt_of_lcoset_type _)
                         ... = card lcs * card H : Sum_const_eq_card_mul

lemma exists_of_lcoset_type (J : lcoset_type G H) :
  ∃ j, j ∈ elt_of J ∧ fin_lcoset H j = elt_of J :=
obtain j Pjin Pj, from has_property J,
exists.intro j (and.intro (Pj ▸ !fin_mem_lcoset) Pj)

lemma lcoset_not_empty (J : lcoset_type G H) : elt_of J ≠ ∅ :=
obtain j Pjin Pj, from has_property J,
assume Pempty, absurd (by rewrite [-Pempty, -Pj]; apply fin_mem_lcoset) (not_mem_empty j)

end lcoset_fintype

section normalizer
open subtype

variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
include ambientG deceqG finG

variable H : finset G

definition normalizer : finset G := {g ∈ univ | ∀ h, h ∈ H → g ∘c h ∈ H}

variable {H}

variable [finsubgH : is_finsubg H]
include finsubgH

lemma subset_normalizer : H ⊆ normalizer H :=
subset_of_forall take g, assume PginH, mem_sep_of_mem !mem_univ
  (take h, assume PhinH, finsubg_conj_closed PginH PhinH)

lemma normalizer_has_one : 1 ∈ normalizer H :=
mem_of_subset_of_mem subset_normalizer (finsubg_has_one H)

lemma normalizer_mul_closed : finset_mul_closed_on (normalizer H) :=
take f g, assume Pfin Pgin,
mem_sep_of_mem !mem_univ take h, assume Phin, begin
  rewrite [-conj_compose],
  apply of_mem_sep Pfin,
  apply of_mem_sep Pgin,
  exact Phin
end

lemma conj_eq_of_mem_normalizer {g : G} : g ∈ normalizer H → image (conj_by g) H = H :=
assume Pgin,
eq_of_card_eq_of_subset (card_image_eq_of_inj_on (take h j, assume P1 P2, !conj_inj))
  (subset_of_forall take h, assume Phin,
  obtain j Pjin Pj, from exists_of_mem_image Phin,
  begin substvars, apply of_mem_sep Pgin, exact Pjin end)

lemma normalizer_has_inv : finset_has_inv (normalizer H) :=
take g, assume Pgin,
mem_sep_of_mem !mem_univ take h, begin
  rewrite [-(conj_eq_of_mem_normalizer Pgin) at {1}, mem_image_iff],
  intro Pex, cases Pex with k Pk,
  rewrite [-(and.right Pk), conj_compose, mul.left_inv, conj_id],
  exact and.left Pk
end

definition normalizer_is_finsubg [instance] : is_finsubg (normalizer H) :=
is_finsubg.mk normalizer_has_one normalizer_mul_closed normalizer_has_inv

lemma lcoset_subset_normalizer (J : lcoset_type (normalizer H) H) :
  elt_of J ⊆ normalizer H :=
lcoset_subset_of_subset J subset_normalizer

lemma lcoset_subset_normalizer_of_mem {g : G} :
  g ∈ normalizer H → fin_lcoset H g ⊆ normalizer H :=
assume Pgin, fin_lcoset_subset subset_normalizer g Pgin

lemma lrcoset_same_of_mem_normalizer {g : G} :
  g ∈ normalizer H → fin_lcoset H g = fin_rcoset H g :=
assume Pg, ext take h, iff.intro
  (assume Pl, obtain j Pjin Pj, from exists_of_mem_image Pl,
  mem_image (of_mem_sep Pg j Pjin)
    (calc g*j*g⁻¹*g = g*j : inv_mul_cancel_right
                ... = h   : Pj))
  (assume Pr, obtain j Pjin Pj, from exists_of_mem_image Pr,
  mem_image (of_mem_sep (finsubg_has_inv (normalizer H) Pg) j Pjin)
    (calc g*(g⁻¹*j*g⁻¹⁻¹) = g*(g⁻¹*j*g)   : inv_inv
                      ... = g*(g⁻¹*(j*g)) : mul.assoc
                      ... = j*g           : mul_inv_cancel_left
                      ... = h             : Pj))

lemma lcoset_mul_eq_lcoset (J K : lcoset_type (normalizer H) H) {g : G} :
  g ∈ elt_of J → (lcoset_mul J K) = fin_lcoset (elt_of K) g :=
assume Pgin,
obtain j Pjin Pj, from has_property J,
obtain k Pkin Pk, from has_property K,
Union_const (lcoset_not_empty J) begin
  rewrite [-Pk], intro h Phin,
  assert Phinn : h ∈ normalizer H,
    apply mem_of_subset_of_mem (lcoset_subset_normalizer_of_mem Pjin),
    rewrite Pj, assumption,
  revert Phin Pgin,
  rewrite [-Pj, *fin_lcoset_same],
  intro Pheq Pgeq,
  rewrite [*(lrcoset_same_of_mem_normalizer Pkin), *fin_lrcoset_comm, Pheq, Pgeq]
end

lemma lcoset_mul_is_lcoset (J K : lcoset_type (normalizer H) H) :
  is_fin_lcoset (normalizer H) H (lcoset_mul J K) :=
obtain j Pjin Pj, from has_property J,
obtain k Pkin Pk, from has_property K,
exists.intro (j*k) (and.intro (finsubg_mul_closed _ Pjin Pkin)
  begin rewrite [lcoset_mul_eq_lcoset J K (Pj ▸ fin_mem_lcoset j), -fin_lcoset_compose, Pk] end)

lemma lcoset_inv_is_lcoset (J : lcoset_type (normalizer H) H) :
  is_fin_lcoset (normalizer H) H (fin_inv (elt_of J)) :=
obtain j Pjin Pj, from has_property J, exists.intro j⁻¹
begin
  rewrite [-Pj, finsubg_inv_lcoset_eq_rcoset],
  apply and.intro,
    apply normalizer_has_inv, assumption,
    apply lrcoset_same_of_mem_normalizer, apply normalizer_has_inv, assumption
end

definition fin_coset_mul (J K : lcoset_type (normalizer H) H) : lcoset_type (normalizer H) H :=
tag (lcoset_mul J K) (lcoset_mul_is_lcoset J K)

definition fin_coset_inv (J : lcoset_type (normalizer H) H) : lcoset_type (normalizer H) H :=
tag (fin_inv (elt_of J)) (lcoset_inv_is_lcoset J)

definition fin_coset_one : lcoset_type (normalizer H) H :=
tag H self_is_lcoset

local infix `^` := fin_coset_mul

lemma fin_coset_mul_eq_lcoset (J K : lcoset_type (normalizer H) H) {g : G} :
  g ∈ (elt_of J) → elt_of (J ^ K) = fin_lcoset (elt_of K) g :=
assume Pgin, lcoset_mul_eq_lcoset J K Pgin

lemma fin_coset_mul_assoc (J K L : lcoset_type (normalizer H) H) :
  J ^ K ^ L = J ^ (K ^ L) :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
obtain k Pkin Pk, from exists_of_lcoset_type K,
assert Pjk : j*k ∈ elt_of (J ^ K), from mul_mem_lcoset_mul J K Pjin Pkin,
obtain l Plin Pl, from has_property L,
subtype.eq (begin
  rewrite [fin_coset_mul_eq_lcoset (J ^ K) _ Pjk,
    fin_coset_mul_eq_lcoset J _ Pjin,
    fin_coset_mul_eq_lcoset K _ Pkin,
    -Pl, *fin_lcoset_compose]
  end)

lemma fin_coset_mul_one (J : lcoset_type (normalizer H) H) :
  J ^ fin_coset_one = J :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
subtype.eq begin
  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ Pjin, -Pj]
end

lemma fin_coset_one_mul (J : lcoset_type (normalizer H) H) :
  fin_coset_one ^ J = J :=
subtype.eq begin
  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ (finsubg_has_one H), fin_lcoset_id]
end

lemma fin_coset_left_inv (J : lcoset_type (normalizer H) H) :
  (fin_coset_inv J) ^ J = fin_coset_one :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
assert Pjinv : j⁻¹ ∈ elt_of (fin_coset_inv J), from inv_mem_fin_inv Pjin,
subtype.eq begin
  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ Pjinv, -Pj, fin_lcoset_inv]
end

variable (H)

definition fin_coset_group [instance] : group (lcoset_type (normalizer H) H) :=
group.mk fin_coset_mul fin_coset_mul_assoc fin_coset_one fin_coset_one_mul fin_coset_mul_one fin_coset_inv fin_coset_left_inv

variables {H} (Hc : finset (lcoset_type (normalizer H) H))

definition fin_coset_Union : finset G := Union Hc elt_of

variables {Hc} [finsubgHc : is_finsubg Hc]
include finsubgHc

lemma mem_normalizer_of_mem_fcU {j : G} : j ∈ fin_coset_Union Hc → j ∈ normalizer H :=
assume Pjin, obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
mem_of_subset_of_mem !lcoset_subset_normalizer PjJ

lemma fcU_has_one : (1:G) ∈ fin_coset_Union Hc :=
iff.elim_right (mem_Union_iff Hc elt_of (1:G))
  (exists.intro 1 (and.intro (finsubg_has_one Hc) (finsubg_has_one H)))

lemma fcU_has_inv : finset_has_inv (fin_coset_Union Hc) :=
take j, assume Pjin, obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
have PJinv : J⁻¹ ∈ Hc, from finsubg_has_inv Hc PJ,
have Pjinv : j⁻¹ ∈ elt_of J⁻¹, from inv_mem_fin_inv PjJ,
iff.elim_right !mem_Union_iff (exists.intro J⁻¹ (and.intro PJinv Pjinv))

lemma fcU_mul_closed : finset_mul_closed_on (fin_coset_Union Hc) :=
take j k, assume Pjin Pkin,
obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
obtain K PK PkK, from iff.elim_left !mem_Union_iff Pkin,
assert Pjk : j*k ∈ elt_of (J*K), from mul_mem_lcoset_mul J K PjJ PkK,
iff.elim_right !mem_Union_iff
  (exists.intro (J*K) (and.intro (finsubg_mul_closed Hc PJ PK) Pjk))

definition fcU_is_finsubg [instance] : is_finsubg (fin_coset_Union Hc) :=
is_finsubg.mk fcU_has_one fcU_mul_closed fcU_has_inv

end normalizer

end group_theory