Quelle  Zassenhaus.thy

(*  Title:      HOL/Algebra/Zassenhaus.thy
  Author: Martin Baillon
*)

section ‹The Zassenhaus Lemma›

theory Zassenhaus
  imports Coset Group_Action
begin

text ‹Proves the second isomorphism theorem and the Zassenhaus lemma.›

subsection ‹Lemmas about normalizer›

lemma (in group) subgroup_in_normalizer:
  assumes "subgroup H G"
  shows "normal H (G(carrier:= (normalizer G H)))"
proof(intro group.normal_invI)
  show "Group.group (G(carrier := normalizer G H))"
    by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
  have K:"H ⊆ (normalizer G H)" unfolding normalizer_def
  proof
    fix x assume xH: "x ∈ H"
    from xH have xG : "x ∈ carrier G" using subgroup.subset assms by auto
    have "x <# H = H"
      by (metis ‹x ∈ H› assms group.lcos_mult_one is_group
         l_repr_independence one_closed subgroup.subset)
    moreover have "H #> inv x = H"
      by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
    ultimately have "x <# H #> (inv x) = H" by simp
    thus " x ∈ stabilizer G (λg. λH∈{H. H ⊆ carrier G}. g <# H #> inv g) H"
      using assms xG subgroup.subset unfolding stabilizer_def by auto
  qed
  thus "subgroup H (G(carrier:= (normalizer G H)))"
    using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
  show  " ∧x h. x ∈ carrier (G(carrier := normalizer G H)) ==> h ∈ H ==>
             x ⊗🪙G(carrier := normalizer G H)🪙 h
               ⊗🪙G(carrier := normalizer G H)🪙 inv🪙G(carrier := normalizer G H)🪙 x ∈ H"
    proof-
    fix x h assume xnorm : "x ∈ carrier (G(carrier := normalizer G H))" and hH : "h ∈ H"
    have xnormalizer:"x ∈ normalizer G H" using xnorm by simp
    moreover have hnormalizer:"h ∈ normalizer G H" using hH K by auto
    ultimately have "x ⊗🪙G(carrier := normalizer G H)🪙 h = x ⊗ h" by simp
    moreover have " inv🪙G(carrier := normalizer G H)🪙 x = inv x"
      using xnormalizer
      by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent)
    ultimately  have xhxegal: "x ⊗🪙G(carrier := normalizer G H)🪙 h
                ⊗🪙G(carrier := normalizer G H)🪙 inv🪙G(carrier := normalizer G H)🪙 x
                  = x ⊗h ⊗ inv x"
      using  hnormalizer by simp
    have  "x ⊗h ⊗ inv x ∈ (x <# H #> inv x)"
      unfolding l_coset_def r_coset_def using hH  by auto
    moreover have "x <# H #> inv x = H"
      using xnormalizer assms subgroup.subset[OF assms]
      unfolding normalizer_def stabilizer_def by auto
    ultimately have "x ⊗h ⊗ inv x ∈ H" by simp
    thus  " x ⊗🪙G(carrier := normalizer G H)🪙 h
               ⊗🪙G(carrier := normalizer G H)🪙 inv🪙G(carrier := normalizer G H)🪙 x ∈ H"
      using xhxegal hH xnorm by simp
  qed
qed


lemma (in group) normal_imp_subgroup_normalizer:
  assumes "subgroup H G"
    and "N ⊲ (G(carrier := H))"
  shows "subgroup H (G(carrier := normalizer G N))"
proof-
  have N_carrierG : "N ⊆ carrier(G)"
    using assms normal_imp_subgroup subgroup.subset
    using incl_subgroup by blast
  {have "H ⊆ normalizer G N" unfolding normalizer_def stabilizer_def
    proof
      fix x assume xH : "x ∈ H"
      hence xcarrierG : "x ∈ carrier(G)" using assms subgroup.subset  by auto
      have " N #> x = x <# N" using assms xH
        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
      hence "x <# N #> inv x =(N #> x) #> inv x"
        by simp
      also have "... = N #> 1"
        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
      thus "x ∈ {g ∈ carrier G. (λH∈{H. H ⊆ carrier G}. g <# H #> inv g) N = N}"
        using xcarrierG by (simp add : N_carrierG)
    qed}
  thus "subgroup H (G(carrier := normalizer G N))"
    using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
      assms normal_imp_subgroup subgroup.subset
    by (metis  group.incl_subgroup is_group)
qed


subsection ‹Second Isomorphism Theorem›

lemma (in group) mult_norm_subgroup:
  assumes "normal N G"
    and "subgroup H G"
  shows "subgroup (N<#>H) G" unfolding subgroup_def
proof-
  have  A :"N <#> H ⊆ carrier G"
    using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)

  have B :"∧ x y. [x ∈ (N <#> H); y ∈ (N <#> H)] ==> (x ⊗ y) ∈ (N<#>H)"
  proof-
    fix x y assume B1a: "x ∈ (N <#> H)"  and B1b: "y ∈ (N <#> H)"
    obtain n1 h1 where B2:"n1 ∈ N ∧ h1 ∈ H ∧ n1⊗h1 = x"
      using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD)
    obtain n2 h2 where B3:"n2 ∈ N ∧ h2 ∈ H ∧ n2⊗h2 = y"
      using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
    have "N #> h1 = h1 <# N"
      using normalI B2 assms normal.coset_eq subgroup.subset by blast
    hence "h1⊗n2 ∈ N #> h1"
      using B2 B3 assms l_coset_def by fastforce
    from this obtain y2 where y2_def:"y2 ∈ N" and y2_prop:"y2⊗h1 = h1⊗n2"
      using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
    have "∧a. a ∈ N ==> a ∈ carrier G"  "∧a. a ∈ H ==> a ∈ carrier G"
      by (meson assms normal_def subgroup.mem_carrier)+
    then have "x⊗y = n1 ⊗ y2 ⊗ h1 ⊗ h2" using y2_def B2 B3
      by (metis (no_types) B2 B3 ‹∧a. a ∈ N ==> a ∈ carrier G› m_assoc m_closed y2_def y2_prop)
    moreover have B4 :"n1 ⊗ y2 ∈N"
      using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def)
    moreover have "h1 ⊗ h2 ∈H" using B2 B3 assms by (simp add: subgroup.m_closed)
    hence "(n1 ⊗ y2) ⊗ (h1 ⊗ h2) ∈(N<#>H) "
      using B4  unfolding set_mult_def by auto
    hence "n1 ⊗ y2 ⊗ h1 ⊗ h2 ∈(N<#>H)"
      using m_assoc B2 B3 assms  normal_imp_subgroup by (metis B4 subgroup.mem_carrier)
    ultimately show  "x ⊗ y ∈ N <#> H" by auto
  qed
  have C :"∧ x. x∈(N<#>H) ==> (inv x)∈(N<#>H)"

  proof-
    fix x assume C1 : "x ∈ (N<#>H)"
    obtain n h where C2:"n ∈ N ∧ h ∈ H ∧ n⊗h = x"
      using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD)
    have C3 :"inv(n⊗h) = inv(h)⊗inv(n)"
      by (meson C2  assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier)
    hence "... ⊗h ∈ N"
      using assms C2
      by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
    hence  C4:"(inv h ⊗ inv n ⊗ h) ⊗ inv h ∈ (N<#>H)"
      using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
    have "inv h ⊗ inv n ⊗ h ⊗ inv h = inv h ⊗ inv n"
      using  subgroup.subset[OF assms(2)]
      by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
    thus "inv(x)∈N<#>H" using C4 C2 C3 by simp
  qed

  have D : "1 ∈ N <#> H"
  proof-
    have D1 : "1 ∈ N"
      using assms by (simp add: normal_def subgroup.one_closed)
     have D2 :"1 ∈ H"
      using assms by (simp add: subgroup.one_closed)
    thus "1 ∈ (N <#> H)"
      using set_mult_def D1 assms by fastforce
  qed
  thus "(N <#> H ⊆ carrier G ∧ (∀x y. x ∈ N <#> H ⟶ y ∈ N <#> H ⟶ x ⊗ y ∈ N <#> H)) ∧
    1 ∈ N <#> H ∧ (∀x. x ∈ N <#> H ⟶ inv x ∈ N <#> H)" using A B C D assms by blast
qed


lemma (in group) mult_norm_sub_in_sub:
  assumes "normal N (G(carrier:=K))"
  assumes "subgroup H (G(carrier:=K))"
  assumes "subgroup K G"
  shows  "subgroup (N<#>H) (G(carrier:=K))"
proof-
  have Hyp:"subgroup (N <#>🪙G(carrier := K)🪙 H) (G(carrier := K))"
    using group.mult_norm_subgroup[where ?G = "G(carrier := K)"] assms subgroup_imp_group by auto
  have "H ⊆ carrier(G(carrier := K))" using assms subgroup.subset by blast
  also have "... ⊆ K" by simp
  finally have Incl1:"H ⊆ K" by simp
  have "N ⊆ carrier(G(carrier := K))" using assms normal_imp_subgroup subgroup.subset by blast
  also have "... ⊆ K" by simp
  finally have Incl2:"N ⊆ K" by simp
  have "(N <#>🪙G(carrier := K)🪙 H) = (N <#> H)"
    using set_mult_consistent by simp
  thus "subgroup (N<#>H) (G(carrier:=K))" using Hyp by auto
qed


lemma (in group) subgroup_of_normal_set_mult:
  assumes "normal N G"
and "subgroup H G"
shows "subgroup H (G(carrier := N <#> H))"
proof-
  have "1 ∈ N" using normal_imp_subgroup assms(1) subgroup_def by blast
  hence "1 <# H ⊆ N <#> H" unfolding set_mult_def l_coset_def by blast
  hence H_incl : "H ⊆ N <#> H"
    by (metis assms(2) lcos_mult_one subgroup_def)
  show "subgroup H (G(carrier := N <#> H))"
  using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] .
qed


lemma (in group) normal_in_normal_set_mult:
  assumes "normal N G"
and "subgroup H G"
shows "normal N (G(carrier := N <#> H))"
proof-
  have "1 ∈ H" using  assms(2) subgroup_def by blast
  hence "N #> 1 ⊆ N <#> H" unfolding set_mult_def r_coset_def by blast
  hence N_incl : "N ⊆ N <#> H"
    by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
  thus "normal N (G(carrier := N <#> H))"
    using normal_Int_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
    by (simp add : inf_absorb1)
qed


proposition (in group) weak_snd_iso_thme:
  assumes "subgroup H G"
    and "N⊲G"
  shows "(G(carrier := N<#>H) Mod N ≅ G(carrier:=H) Mod (N∩H))"
proof-
  define f where "f = (#>) N"
  have GroupNH : "Group.group (G(carrier := N<#>H))"
    using subgroup_imp_group assms mult_norm_subgroup by simp
  have  HcarrierNH :"H ⊆ carrier(G(carrier := N<#>H))"
    using assms subgroup_of_normal_set_mult subgroup.subset by blast
  hence HNH :"H ⊆ N<#>H" by simp
  have op_hom : "f ∈ hom (G(carrier := H)) (G(carrier := N <#> H) Mod N)" unfolding hom_def
  proof
    have "∧x . x ∈ carrier (G(carrier :=H)) ==>
       (#>🪙G(carrier := N <#> H)🪙) N x ∈ carrier (G(carrier := N <#> H) Mod N)"
    proof-
      fix x assume  "x ∈ carrier (G(carrier :=H))"
      hence xH : "x ∈ H" by simp
      hence "(#>🪙G(carrier := N <#> H)🪙) N x ∈ rcosets🪙G(carrier := N <#> H)🪙 N"
        using HcarrierNH RCOSETS_def[where ?G = "G(carrier := N <#> H)"] by blast
      thus "(#>🪙G(carrier := N <#> H)🪙) N x ∈ carrier (G(carrier := N <#> H) Mod N)"
        unfolding FactGroup_def by simp
    qed
    hence "(#>🪙G(carrier := N <#> H)🪙) N ∈ carrier (G(carrier :=H)) →
            carrier (G(carrier := N <#> H) Mod N)" by auto
    hence "f ∈ carrier (G(carrier :=H)) → carrier (G(carrier := N <#> H) Mod N)"
      unfolding r_coset_def f_def  by simp
    moreover have "∧x y. x∈carrier (G(carrier := H)) ==> y∈carrier (G(carrier := H)) ==>
                  f (x ⊗🪙G(carrier := H)🪙 y) = f(x) ⊗🪙G(carrier := N <#> H) Mod N🪙 f(y)"
    proof-
      fix x y assume "x∈carrier (G(carrier := H))" "y∈carrier (G(carrier := H))"
      hence xHyH :"x ∈ H" "y ∈ H" by auto
      have Nxeq :"N #>🪙G(carrier := N<#>H)🪙 x = N #>x" unfolding r_coset_def by simp
      have Nyeq :"N #>🪙G(carrier := N<#>H)🪙 y = N #>y" unfolding r_coset_def by simp

      have "x ⊗🪙G(carrier := H)🪙 y =x ⊗🪙G(carrier := N<#>H)🪙 y" by simp
      hence "N #>🪙G(carrier := N<#>H)🪙 x ⊗🪙G(carrier := H)🪙 y
             = N #>🪙G(carrier := N<#>H)🪙 x ⊗🪙G(carrier := N<#>H)🪙 y" by simp
      also have "... = (N #>🪙G(carrier := N<#>H)🪙 x) <#>🪙G(carrier := N<#>H)🪙
                       (N #>🪙G(carrier := N<#>H)🪙 y)"
        using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y]
             xHyH assms HcarrierNH by auto
      finally show "f (x ⊗🪙G(carrier := H)🪙 y) = f(x) ⊗🪙G(carrier := N <#> H) Mod N🪙 f(y)"
        unfolding  FactGroup_def r_coset_def f_def  using Nxeq Nyeq  by auto
    qed
    hence "(∀x∈carrier (G(carrier := H)). ∀y∈carrier (G(carrier := H)).
           f (x ⊗🪙G(carrier := H)🪙 y) = f(x) ⊗🪙G(carrier := N <#> H) Mod N🪙 f(y))" by blast
    ultimately show  " f ∈ carrier (G(carrier := H)) → carrier (G(carrier := N <#> H) Mod N) ∧
    (∀x∈carrier (G(carrier := H)). ∀y∈carrier (G(carrier := H)).
     f (x ⊗🪙G(carrier := H)🪙 y) = f(x) ⊗🪙G(carrier := N <#> H) Mod N🪙 f(y))"
      by auto
  qed
  hence homomorphism : "group_hom (G(carrier := H)) (G(carrier := N <#> H) Mod N) f"
    unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)]
             normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto
  moreover have im_f :  "(f ` carrier(G(carrier:=H))) = carrier(G(carrier := N <#> H) Mod N)"
  proof
    show  "f ` carrier (G(carrier := H)) ⊆ carrier (G(carrier := N <#> H) Mod N)"
      using op_hom unfolding hom_def using funcset_image by blast
  next
    show "carrier (G(carrier := N <#> H) Mod N) ⊆ f ` carrier (G(carrier := H))"
    proof
      fix x assume p : " x ∈ carrier (G(carrier := N <#> H) Mod N)"
      hence "x ∈ ∪{y. ∃x∈carrier (G(carrier := N <#> H)). y = {N #>🪙G(carrier := N <#> H)🪙 x}}"
        unfolding FactGroup_def RCOSETS_def by auto
      hence hyp :"∃y. ∃h∈carrier (G(carrier := N <#> H)). y = {N #>🪙G(carrier := N <#> H)🪙 h} ∧ x ∈ y"
        using Union_iff by blast
      from hyp obtain nh where nhNH:"nh ∈carrier (G(carrier := N <#> H))"
                          and "x ∈ {N #>🪙G(carrier := N <#> H)🪙 nh}"
        by blast
      hence K: "x = (#>🪙G(carrier := N <#> H)🪙) N nh" by simp
      have "nh ∈ N <#> H" using nhNH by simp
      from this obtain n h where nN : "n ∈ N" and hH : " h ∈ H" and nhnh: "n ⊗ h = nh"
        unfolding set_mult_def by blast
      have  "x = (#>🪙G(carrier := N <#> H)🪙) N (n ⊗ h)" using K nhnh by simp
      hence  "x = (#>) N (n ⊗ h)" using K nhnh unfolding r_coset_def by auto
      also have "... = (N #> n) #>h"
        using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
        by (metis subgroup.mem_carrier)
      finally have "x = (#>) N h"
        using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
      thus "x ∈ f ` carrier (G(carrier := H))" using hH unfolding f_def by simp
    qed
  qed
  moreover have ker_f :"kernel (G(carrier := H)) (G(carrier := N<#>H) Mod N) f = N∩H"
    unfolding kernel_def f_def
    proof-
      have "{x ∈ carrier (G(carrier := H)). N #> x = 1🪙G(carrier := N <#> H) Mod N🪙} =
            {x ∈ carrier (G(carrier := H)). N #> x = N}" unfolding FactGroup_def by simp
      also have "... = {x ∈ carrier (G(carrier := H)). x ∈ N}"
        using coset_join1
        by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group
          normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group)
      also have "... =N ∩ (carrier(G(carrier := H)))" by auto
      finally show "{x ∈ carrier (G(carrier := H)). N#>x = 1🪙G(carrier := N <#> H) Mod N🪙} = N ∩ H"
        by simp
    qed
    ultimately have "(G(carrier := H) Mod N ∩ H) ≅ (G(carrier := N <#> H) Mod N)"
      using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
    hence "G(carrier := N <#> H) Mod N ≅ G(carrier := H) Mod N ∩ H"
      by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_Int_subgroup)
    thus "G(carrier := N <#> H) Mod N ≅ G(carrier := H) Mod N ∩ H" by auto
qed


theorem (in group) snd_iso_thme:
  assumes "subgroup H G"
    and "subgroup N G"
    and "subgroup H (G(carrier:= (normalizer G N)))"
  shows "(G(carrier:= N<#>H) Mod N) ≅ (G(carrier:= H) Mod (H∩N))"
proof-
  have "G(carrier := normalizer G N, carrier := H)
       = G(carrier := H)"  by simp
  hence "G(carrier := normalizer G N, carrier := H) Mod N ∩ H =
         G(carrier := H) Mod N ∩ H" by auto
  moreover have "G(carrier := normalizer G N,
                    carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) =
                G(carrier := N <#>🪙G(carrier := normalizer G N)🪙 H)" by simp
  hence "G(carrier := normalizer G N,
          carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) Mod N =
          G(carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) Mod N" by auto
  hence "G(carrier := normalizer G N,
          carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) Mod N ≅
         G(carrier := normalizer G N, carrier := H) Mod N ∩ H =
          (G(carrier:= N<#>H) Mod N) ≅
         G(carrier := normalizer G N, carrier := H) Mod N ∩ H"
    using subgroup.subset[OF assms(3)]
          subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
    by simp
  ultimately have "G(carrier := normalizer G N,
                    carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) Mod N ≅
                  G(carrier := normalizer G N, carrier := H) Mod N ∩ H =
                 (G(carrier:= N<#>H) Mod N) ≅ G(carrier := H) Mod N ∩ H" by auto
  moreover have "G(carrier := normalizer G N,
                    carrier := N <#>🪙G(carrier := normalizer G N)🪙 H) Mod N ≅
                  G(carrier := normalizer G N, carrier := H) Mod N ∩ H"
    using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
          subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
    by simp
  moreover have "H∩N = N∩H" using assms  by auto
  ultimately show "(G(carrier:= N<#>H) Mod N) ≅ G(carrier := H) Mod H ∩ N" by auto
qed


corollary (in group) snd_iso_thme_recip :
  assumes "subgroup H G"
    and "subgroup N G"
    and "subgroup H (G(carrier:= (normalizer G N)))"
  shows "(G(carrier:= H<#>N) Mod N) ≅ (G(carrier:= H) Mod (H∩N))"
  by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
      normalizer_imp_subgroup snd_iso_thme)


subsection‹The Zassenhaus Lemma›


lemma (in group) distinc:
  assumes "subgroup H G"
    and "H1⊲G(carrier := H)"
    and  "subgroup K G"
    and "K1⊲G(carrier:=K)"
  shows "subgroup (H∩K) (G(carrier:=(normalizer G (H1<#>(H∩K1))) ))"
proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
  show "subgroup (normalizer G (H1 <#> H ∩ K1)) G"
    using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
    by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
next
  show "H ∩ K ⊆ normalizer G (H1 <#> H ∩ K1)" unfolding normalizer_def stabilizer_def
  proof
    fix x assume xHK : "x ∈ H ∩ K"
    hence xG : "{x} ⊆ carrier G" "{inv x} ⊆ carrier G"
      using subgroup.subset assms inv_closed xHK by auto
    have allG : "H ⊆ carrier G" "K ⊆ carrier G" "H1 ⊆ carrier G"  "K1 ⊆ carrier G"
      using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
    have HK1: "H ∩ K1 ⊆ carrier G"
      by (simp add: allG(1) le_infI1)
    have HK1_normal: "H∩K1 ⊲ (G(carrier := H ∩ K))" using normal_inter[OF assms(3)assms(1)assms(4)]
      by (simp add : inf_commute)
    have "H ∩ K ⊆ normalizer G (H ∩ K1)"
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
            assms(1)assms(3)]HK1_normal]] by auto
    hence "x <# (H ∩ K1) #> inv x = (H ∩ K1)"
      using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
                                                            normal_imp_subgroup[OF assms(4)]]]]
      unfolding normalizer_def stabilizer_def by auto
    moreover have "H ⊆ normalizer G H1"
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
    hence "x <# H1 #> inv x = H1"
      using xHK subgroup.subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
      unfolding normalizer_def stabilizer_def by auto
    ultimately have "H1 <#> H ∩ K1 = (x <# H1 #> inv x) <#> (x <# H ∩ K1 #> inv x)" by auto
    also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H ∩ K1 <#> {inv x})"
      by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult)
    also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H ∩ K1 <#> {inv x})"
      using HK1 allG(3) set_mult_assoc setmult_subset_G xG(1) by auto
    also have "... = ({x} <#> H1 <#> {1}) <#> (H ∩ K1 <#> {inv x})"
      using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G)
    also have "... =({x} <#> H1) <#> (H ∩ K1 <#> {inv x})"
      using coset_mult_one r_coset_eq_set_mult[of G H1 1] set_mult_assoc[OF xG(1) allG(3)] allG
      by auto
    also have "... = {x} <#> (H1 <#> H ∩ K1) <#> {inv x}"
      using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
    finally have "H1 <#> H ∩ K1 = x <# (H1 <#> H ∩ K1) #> inv x"
      using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
    thus "x ∈ {g ∈ carrier G. (λH∈{H. H ⊆ carrier G}. g <# H #> inv g) (H1 <#> H ∩ K1)
                                                                       = H1 <#> H ∩ K1}"
      using xG allG setmult_subset_G[OF allG(3), where ?K = "H∩K1"] xHK
      by auto
  qed
qed

lemma (in group) preliminary1:
  assumes "subgroup H G"
    and "H1⊲G(carrier := H)"
    and  "subgroup K G"
    and "K1⊲G(carrier:=K)"
  shows " (H∩K) ∩ (H1<#>(H∩K1)) = (H1∩K)<#>(H∩K1)"
proof
  have all_inclG : "H ⊆ carrier G" "H1 ⊆ carrier G" "K ⊆ carrier G" "K1 ⊆ carrier G"
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
  show "H ∩ K ∩ (H1 <#> H ∩ K1) ⊆ H1 ∩ K <#> H ∩ K1"
  proof
    fix x assume x_def : "x ∈ (H ∩ K) ∩ (H1 <#> (H ∩ K1))"
    from x_def have x_incl : "x ∈ H" "x ∈ K" "x ∈ (H1 <#> (H ∩ K1))" by auto
    then obtain h1 hk1 where h1hk1_def : "h1 ∈ H1" "hk1 ∈ H ∩ K1" "h1 ⊗ hk1 = x"
      using assms unfolding set_mult_def by blast
    hence "hk1 ∈ H ∩ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
    hence "inv hk1 ∈ H ∩ K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
    moreover have "h1 ⊗ hk1 ∈ H ∩ K" using x_incl h1hk1_def by auto
    ultimately have "h1 ⊗ hk1 ⊗ inv hk1 ∈ H ∩ K"
      using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
    hence "h1 ∈ H ∩ K" using  h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
      by (metis Int_iff contra_subsetD inv_solve_right m_closed)
    hence "h1 ∈ H1 ∩ H ∩ K" using h1hk1_def by auto
    hence "h1 ∈ H1 ∩ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
    hence "h1 ⊗ hk1 ∈ (H1∩K)<#>(H∩K1)"
      using h1hk1_def unfolding set_mult_def by auto
    thus " x ∈ (H1∩K)<#>(H∩K1)" using h1hk1_def x_def by auto
  qed
  show "H1 ∩ K <#> H ∩ K1 ⊆ H ∩ K ∩ (H1 <#> H ∩ K1)"
  proof-
    have "H1 ∩ K ⊆ H ∩ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
    moreover have "H ∩ K1 ⊆ H ∩ K"
      using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
    ultimately have "H1 ∩ K <#> H ∩ K1 ⊆ H ∩ K" unfolding set_mult_def
      using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
    moreover have "H1 ∩ K ⊆ H1" by auto
    hence "H1 ∩ K <#> H ∩ K1 ⊆ (H1 <#> H ∩ K1)" unfolding set_mult_def by auto
    ultimately show "H1 ∩ K <#> H ∩ K1 ⊆ H ∩ K ∩ (H1 <#> H ∩ K1)" by auto
  qed
qed

lemma (in group) preliminary2:
  assumes "subgroup H G"
    and "H1⊲G(carrier := H)"
    and  "subgroup K G"
    and "K1⊲G(carrier:=K)"
  shows "(H1<#>(H∩K1)) ⊲ G(carrier:=(H1<#>(H∩K)))"
proof-
  have all_inclG : "H ⊆ carrier G" "H1 ⊆ carrier G" "K ⊆ carrier G" "K1 ⊆ carrier G"
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
  have subH1:"subgroup (H1 <#> H ∩ K) (G(carrier := H))"
    using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
          assms(1)]] assms by auto
  have "Group.group (G(carrier:=(H1<#>(H∩K))))"
    using  subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]].
  moreover have subH2 : "subgroup (H1 <#> H ∩ K1) (G(carrier := H))"
    using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
  hence "(H∩K1) ⊆ (H∩K)"
    using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
    by (metis inf.mono  partial_object.simps(1) partial_object.update_convs(1) subset_refl)
  hence incl:"(H1<#>(H∩K1)) ⊆ H1<#>(H∩K)" using assms subgroup.subset normal_imp_subgroup
    unfolding set_mult_def by blast
  hence "subgroup (H1 <#> H ∩ K1) (G(carrier := (H1<#>(H∩K))))"
    using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
          subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
  moreover have " (∧ x. x∈carrier (G(carrier := H1 <#> H ∩ K)) ==>
        H1 <#> H∩K1 #>🪙G(carrier := H1 <#> H∩K)🪙 x = x <#🪙G(carrier := H1 <#> H∩K)🪙 (H1 <#> H∩K1))"
  proof-
    fix x assume  "x ∈carrier (G(carrier := H1 <#> H ∩ K))"
    hence x_def : "x ∈ H1 <#> H ∩ K" by simp
    from this obtain h1 hk where h1hk_def :"h1 ∈ H1" "hk ∈ H ∩ K" "h1 ⊗ hk = x"
      unfolding set_mult_def by blast
    have HK1: "H ∩ K1 ⊆ carrier G"
      by (simp add: all_inclG(1) le_infI1)
    have xH : "x ∈ H" using subgroup.subset[OF subH1] using x_def by auto
    hence allG : "h1 ∈ carrier G" "hk ∈ carrier G" "x ∈ carrier G"
      using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
    hence "x <#🪙G(carrier := H1 <#> H∩K)🪙 (H1 <#> H∩K1) =h1 ⊗ hk <# (H1 <#> H∩K1)"
      using subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    also have "... = h1 <# (hk <# (H1 <#> H∩K1))"
      using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
      by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
    also have "... = h1 <# (hk <# H1 <#> H∩K1)"
      using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
    also have "... = h1 <# (hk <# H1 #> 1 <#> H∩K1 #> 1)"
      using coset_mult_one allG all_inclG l_coset_subset_G
      by (simp add: inf.coboundedI2 setmult_subset_G)
    also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H∩K1 #> inv hk #> hk)"
      using all_inclG allG coset_mult_assoc l_coset_subset_G
      by (simp add: inf.coboundedI1 setmult_subset_G)
    finally have "x <#🪙G(carrier := H1 <#> H ∩ K)🪙 (H1 <#> H ∩ K1)
                  = h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H∩K1 #> inv hk) #> hk)"
      using rcos_assoc_lcos allG all_inclG HK1
      by (simp add: l_coset_subset_G r_coset_subset_G setmult_rcos_assoc)
    moreover have "H ⊆ normalizer G H1"
      using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
    hence "∧g. g ∈ H ==> g ∈ {g ∈ carrier G. (λH∈{H. H ⊆ carrier G}. g <# H #> inv g) H1 = H1}"
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
    hence "∧g. g ∈ H ==> g <# H1 #> inv g = H1" using all_inclG by simp
    hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
    moreover have "H∩K ⊆ normalizer G (H∩K1)"
      using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
            subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
    hence "∧g. g∈H∩K ==> g∈{g∈carrier G. (λH∈{H. H ⊆ carrier G}. g <# H #> inv g) (H∩K1) = H∩K1}"
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
    hence "∧g. g ∈ H∩K ==> g <# (H∩K1) #> inv g = H∩K1"
      using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
            assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
    hence "(hk <# H∩K1 #> inv hk) = H∩K1" using h1hk_def by simp
    ultimately have "x <#🪙G(carrier := H1 <#> H ∩ K)🪙 (H1 <#> H ∩ K1) = h1 <#(H1 <#> (H ∩ K1)#> hk)"
      by auto
    also have "... = h1 <# H1 <#> ((H ∩ K1)#> hk)"
      using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H ∩ K1)#> hk"] allG all_inclG
      by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc)
    also have "... = H1 <#> ((H ∩ K1)#> hk)"
      using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def
      by auto
    finally have eq1 : "x <#🪙G(carrier := H1 <#> H ∩ K)🪙 (H1 <#> H ∩ K1) = H1 <#> (H ∩ K1) #> hk"
      by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
    have "H1 <#> H ∩ K1 #>🪙G(carrier := H1 <#> H ∩ K)🪙 x = H1 <#> H ∩ K1 #> (h1 ⊗ hk)"
      using subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    also have "... = H1 <#> H ∩ K1 #> h1 #> hk"
      using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
    also have"... = H ∩ K1 <#> H1 #> h1 #> hk"
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
    also have "... = H ∩ K1 <#> H1 #> hk"
      using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup]
            h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc)
    finally  have "H1 <#> H ∩ K1 #>🪙G(carrier := H1 <#> H ∩ K)🪙 x =H1 <#> H ∩ K1 #> hk"
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
    thus " H1 <#> H ∩ K1 #>🪙G(carrier := H1 <#> H ∩ K)🪙 x =
             x <#🪙G(carrier := H1 <#> H ∩ K)🪙 (H1 <#> H ∩ K1)" using eq1 by simp
  qed
  ultimately show "H1 <#> H ∩ K1 ⊲ G(carrier := H1 <#> H ∩ K)"
    unfolding normal_def normal_axioms_def by auto
qed


proposition (in group)  Zassenhaus_1:
  assumes "subgroup H G"
    and "H1⊲G(carrier := H)"
    and  "subgroup K G"
    and "K1⊲G(carrier:=K)"
  shows "(G(carrier:= H1 <#> (H∩K)) Mod (H1<#>H∩K1)) ≅ (G(carrier:= (H∩K)) Mod ((H1∩K)<#>(H∩K1)))"
proof-
  define N  and N1 where "N = (H∩K)" and "N1 =H1<#>(H∩K1)"
  have normal_N_N1 : "subgroup N (G(carrier:=(normalizer G N1)))"
    by (simp add: N1_def N_def assms distinc normal_imp_subgroup)
  have Hp:"(G(carrier:= N<#>N1) Mod N1) ≅ (G(carrier:= N) Mod (N∩N1))"
  by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub
        normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair)
  have H_simp: "N<#>N1 = H1<#> (H∩K)"
  proof-
    have H1_incl_G : "H1 ⊆ carrier G"
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
    have K1_incl_G :"K1 ⊆ carrier G"
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
    have "N<#>N1= (H∩K)<#> (H1<#>(H∩K1))" by (auto simp add: N_def N1_def)
    also have "... = ((H∩K)<#>H1) <#>(H∩K1)"
      using set_mult_assoc[where ?M = "H∩K"] K1_incl_G H1_incl_G assms
      by (simp add: inf.coboundedI2 subgroup.subset)
    also have "... = (H1<#>(H∩K))<#>(H∩K1)"
      using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
    also have "... = H1 <#> ((H∩K)<#>(H∩K1))"
      using set_mult_assoc K1_incl_G H1_incl_G assms
      by (simp add: inf.coboundedI2 subgroup.subset)
    also have " ((H∩K)<#>(H∩K1)) = (H∩K)"
    proof (intro set_mult_subgroup_idem[where ?H = "H∩K" and ?N="H∩K1",
             OF subgroups_Inter_pair[OF assms(1) assms(3)]])
      show "subgroup (H ∩ K1) (G(carrier := H ∩ K))"
        using subgroup_incl[where ?I = "H∩K1" and ?J = "H∩K",OF subgroups_Inter_pair[OF assms(1)
              incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
              normal_imp_subgroup by (metis inf_commute normal_inter)
    qed
    hence " H1 <#> ((H∩K)<#>(H∩K1)) = H1 <#> ((H∩K))"
      by simp
    thus "N <#> N1 = H1 <#> H ∩ K"
      by (simp add: calculation)
  qed

  have "N∩N1 = (H1∩K)<#>(H∩K1)"
    using preliminary1 assms N_def N1_def by simp
  thus  "(G(carrier:= H1 <#> (H∩K)) Mod N1) ≅ (G(carrier:= N) Mod ((H1∩K)<#>(H∩K1)))"
    using H_simp Hp by auto
qed


theorem (in group) Zassenhaus:
  assumes "subgroup H G"
    and "H1⊲G(carrier := H)"
    and  "subgroup K G"
    and "K1⊲G(carrier:=K)"
  shows "(G(carrier:= H1 <#> (H∩K)) Mod (H1<#>(H∩K1))) ≅
         (G(carrier:= K1 <#> (H∩K)) Mod (K1<#>(K∩H1)))"
proof-
  define Gmod1 Gmod2 Gmod3 Gmod4
    where "Gmod1 = (G(carrier:= H1 <#> (H∩K)) Mod (H1<#>(H∩K1))) "
      and "Gmod2 = (G(carrier:= K1 <#> (K∩H)) Mod (K1<#>(K∩H1)))"
      and "Gmod3 = (G(carrier:= (H∩K)) Mod ((H1∩K)<#>(H∩K1)))"
      and "Gmod4 = (G(carrier:= (K∩H)) Mod ((K1∩H)<#>(K∩H1)))"
  have Hyp :  "Gmod1 ≅ Gmod3" "Gmod2 ≅ Gmod4"
    using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto
  have Hp : "Gmod3 = G(carrier:= (K∩H)) Mod ((K∩H1)<#>(K1∩H))"
    by (simp add: Gmod3_def inf_commute)
  have "(K∩H1)<#>(K1∩H) = (K1∩H)<#>(K∩H1)"
  proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]])
    show "K1 ∩ H ⊲ G(carrier := H ∩ K)"
      using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
   next
    show "subgroup (K ∩ H1) (G(carrier := H ∩ K))"
      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
  qed
  hence  "Gmod3 = Gmod4" using Hp Gmod4_def by simp
  hence "Gmod1 ≅ Gmod2"
    by (metis assms group.iso_sym iso_trans Hyp normal.factorgroup_is_group Gmod2_def preliminary2)
  thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
qed

end