Theory JordanHolder

(*  Title:      The Jordan-Hölder Theorem
    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
*)

theory JordanHolder
imports
  CompositionSeries
  MaximalNormalSubgroups
  "HOL-Library.Multiset"
  GroupIsoClasses
begin

section ‹The Jordan-H\"older Theorem›

locale jordan_hoelder = group
  + compℌ?: composition_series G ℌ
  + comp𝔊?: composition_series G 𝔊 for ℌ and 𝔊
  + assumes finite: "finite (carrier G)"

text ‹Before we finally start the actual proof of the theorem, one last lemma: Cancelling
  the last entry of a normal series results in a normal series with quotients being all but the last
  of the original ones.›

lemma (in normal_series) quotients_butlast:
  assumes "length 𝔊 > 1"
  shows "butlast quotients = normal_series.quotients (G⦇carrier := 𝔊 ! (length 𝔊 - 1 - 1)⦈) (take (length 𝔊 - 1) 𝔊)"
proof (rule nth_equalityI )
  define n where "n = length 𝔊 - 1"
  hence "n = length (take n 𝔊)" "n > 0" "n < length 𝔊" using assms notempty by auto
  interpret normal𝔊butlast: normal_series "(G⦇carrier := 𝔊 ! (n - 1)⦈)" "take n 𝔊" 
    using normal_series_prefix_closed ‹n > 0› ‹n < length 𝔊› by auto
  have "length (butlast quotients) = length quotients - 1" by (metis length_butlast)
  also have "… = length 𝔊 - 1 - 1" by (metis add_diff_cancel_right' quotients_length)
  also have "… = length (take n 𝔊) - 1" by (metis ‹n = length (take n 𝔊)› n_def)
  also have "… = length normal𝔊butlast.quotients" by (metis normal𝔊butlast.quotients_length diff_add_inverse2)
  finally show "length (butlast quotients) = length normal𝔊butlast.quotients" .
  have "∀i<length (butlast quotients). butlast quotients ! i = normal𝔊butlast.quotients ! i"
  proof auto
    fix i
    assume i: "i < length quotients - Suc 0"
    hence i': "i < length 𝔊 - 1" "i < n" "i + 1 < n" unfolding n_def using quotients_length by auto
    from i have "butlast quotients ! i = quotients ! i" by (metis One_nat_def length_butlast nth_butlast)
    also have "… = G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i" unfolding quotients_def using i'(1) by auto
    also have "… = G⦇carrier := (take n 𝔊) ! (i + 1)⦈ Mod (take n 𝔊) ! i" using i'(2,3) nth_take by metis
    also have "… = normal𝔊butlast.quotients ! i" unfolding normal𝔊butlast.quotients_def using i' by fastforce
    finally show "butlast (normal_series.quotients G 𝔊) ! i = normal_series.quotients (G⦇carrier := 𝔊 ! (n - Suc 0)⦈) (take n 𝔊) ! i" by auto
  qed
  thus "⋀i. i < length (butlast quotients) 
            ⟹ butlast quotients ! i
              = normal_series.quotients (G⦇carrier := 𝔊 ! (length 𝔊 - 1 - 1)⦈)  (take (length 𝔊 - 1) 𝔊) ! i"
    unfolding n_def by auto
qed

text ‹The main part of the Jordan Hölder theorem is its statement about the uniqueness of 
  a composition series. Here, uniqueness up to reordering and isomorphism is modelled by stating
  that the multisets of isomorphism classes of all quotients are equal.›

theorem jordan_hoelder_multisets:
  assumes "group G"
  assumes "finite (carrier G)"
  assumes "composition_series G 𝔊"
  assumes "composition_series G ℌ"
  shows "mset (map group.iso_class (normal_series.quotients G 𝔊))
    = mset (map group.iso_class (normal_series.quotients G ℌ))"
using assms
proof (induction "length 𝔊" arbitrary: 𝔊 ℌ G rule: full_nat_induct)
  case (1 𝔊 ℌ G)
  then interpret comp𝔊: composition_series G 𝔊 by simp
  from 1 interpret compℌ: composition_series G ℌ by simp
  from 1 interpret grpG: group G by simp
  show ?case
  proof (cases "length 𝔊 ≤ 2")
  next
    case True
    hence  "length 𝔊 = 0 ∨ length 𝔊 = 1 ∨ length 𝔊 = 2" by arith
    with comp𝔊.notempty have  "length 𝔊 = 1 ∨ length 𝔊 = 2" by simp
    thus ?thesis
    proof (auto simp del: mset_map)
      ― ‹First trivial case: @{text 𝔊} is the trivial group.›
      assume "length 𝔊 = Suc 0"
      hence length: "length 𝔊 = 1" by simp
      hence "length [] + 1 = length 𝔊" by auto
      moreover from length have char𝔊: "𝔊 = [{𝟭⇘G⇙}]" by (metis comp𝔊.composition_series_length_one)
      hence "carrier G = {𝟭⇘G⇙}" by (metis comp𝔊.composition_series_triv_group)
      with length char𝔊 have "𝔊 = ℌ" using compℌ.composition_series_triv_group by simp
      thus ?thesis by simp
    next
      ― ‹Second trivial case: @{text 𝔊} is simple.›
      assume "length 𝔊 = 2"
      hence 𝔊char: "𝔊 = [{𝟭⇘G⇙}, carrier G]" by (metis comp𝔊.length_two_unique)
      hence simple: "simple_group G" by (metis comp𝔊.composition_series_simple_group)
      hence "ℌ = [{𝟭⇘G⇙}, carrier G]" using compℌ.composition_series_simple_group by auto
      with 𝔊char have "𝔊 = ℌ" by simp
      thus ?thesis by simp
    qed
  next
    case False
    ― ‹Non-trivial case: @{text 𝔊} has length at least 3.›
    hence length: "length 𝔊 ≥ 3" by simp
    ― ‹First we show that @{text ℌ} must have a length of at least 3.›
    hence "¬ simple_group G" using comp𝔊.composition_series_simple_group by auto
    hence "ℌ ≠ [{𝟭⇘G⇙}, carrier G]" using compℌ.composition_series_simple_group by auto
    hence "length ℌ ≠ 2" using compℌ.length_two_unique by auto
    moreover from length have "carrier G ≠ {𝟭⇘G⇙}" using comp𝔊.composition_series_length_one comp𝔊.composition_series_triv_group by auto
    hence "length ℌ ≠ 1" using compℌ.composition_series_length_one compℌ.composition_series_triv_group by auto
    moreover from compℌ.notempty have "length ℌ ≠ 0" by simp
    ultimately have lengthℌbig: "length ℌ ≥ 3" using compℌ.notempty by arith
    define m where "m = length ℌ - 1"
    define n where "n = length 𝔊 - 1"
    from lengthℌbig have m': "m > 0" "m < length ℌ" "(m - 1) + 1 < length ℌ" "m - 1 = length ℌ - 2" "m - 1 + 1 = length ℌ - 1" "m - 1 < length ℌ"
      unfolding m_def by auto
    from length have n': "n > 0" "n < length 𝔊" "(n - 1) + 1 < length 𝔊" "n - 1 < length 𝔊" "Suc n ≤ length 𝔊"
     "n - 1 = length 𝔊 - 2" "n - 1 + 1 = length 𝔊 - 1"  unfolding n_def by auto
    define 𝔊Pn where "𝔊Pn = G⦇carrier := 𝔊 ! (n - 1)⦈"
    define ℌPm where "ℌPm = G⦇carrier := ℌ ! (m - 1)⦈"
    then interpret grp𝔊Pn: group 𝔊Pn unfolding 𝔊Pn_def using n' by (metis comp𝔊.normal_series_subgroups comp𝔊.subgroup_imp_group)
    interpret grpℌPm: group ℌPm unfolding ℌPm_def using m' compℌ.normal_series_subgroups 1(2) group.subgroup_imp_group by force
    have finGbl: "finite (carrier 𝔊Pn)" using ‹n - 1 < length 𝔊› 1(3) unfolding 𝔊Pn_def using comp𝔊.normal_series_subgroups comp𝔊.subgroup_finite by auto
    have finHbl: "finite (carrier ℌPm)" using ‹m - 1 < length ℌ› 1(3) unfolding ℌPm_def using compℌ.normal_series_subgroups comp𝔊.subgroup_finite by auto
    have quots𝔊notempty: "comp𝔊.quotients ≠ []" using comp𝔊.quotients_length length by auto
    have quotsℌnotempty: "compℌ.quotients ≠ []" using compℌ.quotients_length lengthℌbig by auto
    
    ― ‹Instantiate truncated composition series since they are used for both cases›
    interpret ℌbutlast: composition_series ℌPm "take m ℌ" using compℌ.composition_series_prefix_closed m'(1,2) ℌPm_def by auto
    interpret 𝔊butlast: composition_series 𝔊Pn "take n 𝔊" using comp𝔊.composition_series_prefix_closed n'(1,2) 𝔊Pn_def by auto
    have ltaken: "n = length (take n 𝔊)" using length_take n'(2) by auto
    have ltakem: "m = length (take m ℌ)" using length_take m'(2) by auto
    show ?thesis
    proof (cases "ℌ ! (m - 1)  = 𝔊 ! (n - 1)")
      ― ‹If @{term "ℌ ! (l - 1) = 𝔊 ! 1"}, everything is simple...›
      case True
      ― ‹The last quotients of @{term 𝔊} and @{term ℌ} are equal.›
      have lasteq: "last comp𝔊.quotients = last compℌ.quotients"
      proof -
        from length have lg: "length 𝔊 - 1 - 1 + 1 = length 𝔊 - 1" by (metis Suc_diff_1 Suc_eq_plus1 n'(1) n_def)
        from lengthℌbig have lh: "length ℌ - 1 - 1 + 1 = length ℌ - 1" by (metis Suc_diff_1 Suc_eq_plus1 ‹0 < m› m_def)
        have "last comp𝔊.quotients =  G Mod 𝔊 ! (n - 1)" using length comp𝔊.last_quotient unfolding n_def by auto
        also have "… = G Mod ℌ ! (m - 1)" using True by simp
        also have "… = last compℌ.quotients" using lengthℌbig compℌ.last_quotient unfolding m_def by auto
        finally show ?thesis .
      qed
      from ltaken have ind: "mset (map group.iso_class 𝔊butlast.quotients) = mset (map group.iso_class ℌbutlast.quotients)"
        using 1(1) True n'(5) grp𝔊Pn.is_group finGbl 𝔊butlast.is_composition_series ℌbutlast.is_composition_series unfolding 𝔊Pn_def ℌPm_def by metis
      have "mset (map group.iso_class comp𝔊.quotients)
                    = mset (map group.iso_class (butlast comp𝔊.quotients @ [last comp𝔊.quotients]))" by (simp add: quots𝔊notempty)
      also have "… = mset (map group.iso_class (𝔊butlast.quotients @ [last (comp𝔊.quotients)]))" using comp𝔊.quotients_butlast length unfolding n_def 𝔊Pn_def by auto
      also have "… = mset ((map group.iso_class 𝔊butlast.quotients) @ [group.iso_class (last (comp𝔊.quotients))])" by auto
      also have "… = mset (map group.iso_class 𝔊butlast.quotients) + {# group.iso_class (last (comp𝔊.quotients)) #}" by auto
      also have "… = mset (map group.iso_class ℌbutlast.quotients) + {# group.iso_class (last (comp𝔊.quotients)) #}" using ind by simp
      also have "… = mset (map group.iso_class ℌbutlast.quotients) + {# group.iso_class (last (compℌ.quotients)) #}" using lasteq by simp
      also have "… = mset ((map group.iso_class ℌbutlast.quotients) @ [group.iso_class (last (compℌ.quotients))])" by auto
      also have "… = mset (map group.iso_class (ℌbutlast.quotients @ [last (compℌ.quotients)]))" by auto
      also have "… = mset (map group.iso_class (butlast compℌ.quotients @ [last compℌ.quotients]))" using lengthℌbig compℌ.quotients_butlast unfolding m_def ℌPm_def by auto
      also have "… = mset (map group.iso_class compℌ.quotients)" using append_butlast_last_id quotsℌnotempty by simp
      finally show ?thesis .
    next
      case False 
      define ℌPmInt𝔊Pn where "ℌPmInt𝔊Pn = G⦇carrier := ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)⦈"
      interpret 𝔊Pnmax: max_normal_subgroup "𝔊 ! (n - 1)" G unfolding n_def
        by (metis add_lessD1 diff_diff_add n'(3) add.commute one_add_one 1(3) comp𝔊.snd_to_last_max_normal)
      interpret ℌPmmax: max_normal_subgroup "ℌ ! (m - 1)" G unfolding m_def
        by (metis add_lessD1 diff_diff_add m'(3) add.commute one_add_one 1(3) compℌ.snd_to_last_max_normal)
      have ℌPmnormG: "ℌ ! (m - 1) ⊲ G" using compℌ.normal_series_snd_to_last m'(4) unfolding m_def by auto
      have 𝔊PnnormG: "𝔊 ! (n - 1) ⊲ G" using comp𝔊.normal_series_snd_to_last n'(6) unfolding n_def by auto
      have ℌPmint𝔊PnnormG: "ℌ ! (m - 1) ∩ 𝔊 ! (n - 1) ⊲ G" using ℌPmnormG 𝔊PnnormG by (rule comp𝔊.normal_subgroup_intersect)
      have Intnorm𝔊Pn: "ℌ ! (m - 1) ∩ 𝔊 ! (n - 1) ⊲ 𝔊Pn" using 𝔊PnnormG ℌPmnormG Int_lower2 unfolding 𝔊Pn_def
        by (metis comp𝔊.normal_restrict_supergroup comp𝔊.normal_series_subgroups comp𝔊.normal_subgroup_intersect n'(4))
      then interpret grp𝔊PnModℌPmint𝔊Pn: group "𝔊Pn Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)" by (rule normal.factorgroup_is_group)
      have IntnormℌPm: "ℌ ! (m - 1) ∩ 𝔊 ! (n - 1) ⊲ ℌPm" using ℌPmnormG 𝔊PnnormG Int_lower2 Int_commute unfolding ℌPm_def
        by (metis comp𝔊.normal_restrict_supergroup comp𝔊.normal_subgroup_intersect compℌ.normal_series_subgroups m'(6))
      then interpret grpℌPmModℌPmint𝔊Pn: group "ℌPm Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)" by (rule normal.factorgroup_is_group)

      ― ‹Show that the second to last entries are not contained in each other.›
      have notℌPmSub𝔊Pn: "¬ (ℌ ! (m - 1) ⊆ 𝔊 ! (n - 1))" using ℌPmmax.max_normal 𝔊PnnormG False[symmetric] 𝔊Pnmax.proper by simp
      have not𝔊PnSubℌPm: "¬ (𝔊 ! (n - 1) ⊆ ℌ ! (m - 1))" using 𝔊Pnmax.max_normal ℌPmnormG False ℌPmmax.proper by simp
      
      ― ‹Show that @{term "G Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1))"} is a simple group.›
      have ℌPmSubSetmult: "ℌ ! (m - 1) ⊆ ℌ ! (m - 1) <#>⇘G⇙ 𝔊 ! (n - 1)"
        using 𝔊Pnmax.subgroup_axioms ℌPmnormG second_isomorphism_grp.H_contained_in_set_mult 
          second_isomorphism_grp_axioms_def second_isomorphism_grp_def by blast
      have 𝔊PnSubSetmult: "𝔊 ! (n - 1) ⊆ ℌ ! (m - 1) <#>⇘G⇙ 𝔊 ! (n - 1)"
        by (metis 𝔊Pnmax.subset 𝔊PnnormG ℌPmSubSetmult ℌPmmax.max_normal ℌPmmax.subgroup_axioms ℌPmnormG 
            comp𝔊.normal_subgroup_set_mult_closed comp𝔊.set_mult_inclusion)
      have "𝔊 ! (n - 1) ≠ (ℌ ! (m - 1)) <#>⇘G⇙ (𝔊 ! (n - 1))" using ℌPmSubSetmult notℌPmSub𝔊Pn by auto
      hence set_multG: "(ℌ ! (m - 1)) <#>⇘G⇙ (𝔊 ! (n - 1)) = carrier G"
        by (metis 𝔊PnSubSetmult 𝔊Pnmax.max_normal 𝔊PnnormG ℌPmnormG comp𝔊.normal_subgroup_set_mult_closed)
      then obtain φ where "φ ∈ iso (𝔊Pn Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1))) (G⦇carrier := carrier G⦈ Mod ℌ ! (m - 1))"
        by (metis second_isomorphism_grp.normal_intersection_quotient_isom ℌPmnormG  
            𝔊Pn_def 𝔊Pnmax.subgroup_axioms second_isomorphism_grp_axioms_def second_isomorphism_grp_def)
      hence φ: "φ ∈ iso (𝔊Pn Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1))) (G Mod ℌ ! (m - 1))" by auto
      then obtain φ2 where φ2: "φ2 ∈ iso (G Mod ℌ ! (m - 1)) (𝔊Pn Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)))"
        using group.iso_set_sym grp𝔊PnModℌPmint𝔊Pn.is_group by auto
      moreover have "simple_group (G⦇carrier := ℌ ! (m - 1 + 1)⦈ Mod ℌ ! (m - 1))" using compℌ.simplefact m'(3) by simp
      hence "simple_group (G Mod ℌ ! (m - 1))" using compℌ.last last_conv_nth compℌ.notempty m'(5) by fastforce
      ultimately have simple𝔊PnModInt: "simple_group (𝔊Pn Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)))"
        using simple_group.iso_simple grp𝔊PnModℌPmint𝔊Pn.is_group by auto
      interpret grpGModℌPm: group "(G Mod ℌ ! (m - 1))" by (metis ℌPmnormG normal.factorgroup_is_group)

      ― ‹Show analogues of the previous statements for @{term "ℌ ! (m - 1)"} instead of @{term "𝔊 ! (n - 1)"}.›
      have ℌPmSubSetmult': "ℌ ! (m - 1) ⊆ 𝔊 ! (n - 1) <#>⇘G⇙ ℌ ! (m - 1)"
        by (metis 𝔊PnnormG ℌPmSubSetmult comp𝔊.commut_normal ℌPmnormG normal_imp_subgroup)
      have 𝔊PnSubSetmult': "𝔊 ! (n - 1) ⊆ 𝔊 ! (n - 1) <#>⇘G⇙ ℌ ! (m - 1)"
        by (metis ℌPmnormG normal_imp_subgroup 𝔊PnSubSetmult 𝔊PnnormG comp𝔊.commut_normal)
      have "ℌ ! (m - 1) ≠ (𝔊 ! (n - 1)) <#>⇘G⇙ (ℌ ! (m - 1))" using 𝔊PnSubSetmult' not𝔊PnSubℌPm by auto
      hence set_multG: "(𝔊 ! (n - 1)) <#>⇘G⇙ (ℌ ! (m - 1)) = carrier G"
        using ℌPmmax.max_normal 𝔊PnnormG comp𝔊.normal_subgroup_set_mult_closed ℌPmSubSetmult' ℌPmnormG by blast
      from set_multG obtain ψ where 
            "ψ ∈ iso (ℌPm Mod (𝔊 ! (n - 1) ∩ ℌ ! (m - 1))) (G⦇carrier := carrier G⦈ Mod 𝔊 ! (n - 1))"
        by (metis ℌPm_def ℌPmnormG second_isomorphism_grp_axioms_def second_isomorphism_grp_def 
            second_isomorphism_grp.normal_intersection_quotient_isom 𝔊PnnormG normal_imp_subgroup)

      hence ψ: "ψ ∈ iso (ℌPm Mod (ℌ ! (m - 1) ∩ (𝔊 ! (n - 1)))) (G⦇carrier := carrier G⦈ Mod 𝔊 ! (n - 1))" using Int_commute by metis
      then obtain ψ2 where
             ψ2: "ψ2 ∈ iso (G Mod 𝔊 ! (n - 1)) (ℌPm Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)))"
        using group.iso_set_sym grpℌPmModℌPmint𝔊Pn.is_group by auto
      moreover have "simple_group (G⦇carrier := 𝔊 ! (n - 1 + 1)⦈ Mod 𝔊 ! (n - 1))" using comp𝔊.simplefact n'(3) by simp
      hence "simple_group (G Mod 𝔊 ! (n - 1))" using comp𝔊.last last_conv_nth comp𝔊.notempty n'(7) by fastforce
      ultimately have simpleℌPmModInt: "simple_group (ℌPm Mod (ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)))" 
        using simple_group.iso_simple grpℌPmModℌPmint𝔊Pn.is_group by auto
      interpret grpGMod𝔊Pn: group "(G Mod 𝔊 ! (n - 1))" by (metis 𝔊PnnormG normal.factorgroup_is_group)
      
      ― ‹Instantiate several composition series used to build up the equality of quotient multisets.›
      define 𝔎 where "𝔎 = remdups_adj (map ((∩) (ℌ ! (m - 1))) 𝔊)"
      define 𝔏 where "𝔏 = remdups_adj (map ((∩) (𝔊 ! (n - 1))) ℌ)"
      interpret 𝔎: composition_series ℌPm 𝔎 using comp𝔊.intersect_normal 1(3) ℌPmnormG unfolding 𝔎_def ℌPm_def by auto
      interpret 𝔏: composition_series 𝔊Pn 𝔏 using compℌ.intersect_normal 1(3) 𝔊PnnormG unfolding 𝔏_def 𝔊Pn_def by auto


      ― ‹Apply the induction hypothesis on @{text 𝔊butlast} and @{text 𝔏}›
      from n'(2) have "Suc (length (take n 𝔊)) ≤ length 𝔊" by auto
      hence multisets𝔊butlast𝔏: "mset (map group.iso_class 𝔊butlast.quotients) = mset (map group.iso_class 𝔏.quotients)"
        using  "1.hyps" grp𝔊Pn.is_group finGbl 𝔊butlast.is_composition_series 𝔏.is_composition_series by metis
      hence length𝔏: "n = length 𝔏" using 𝔊butlast.quotients_length 𝔏.quotients_length length_map size_mset ltaken by metis
      hence length𝔏': "length 𝔏 > 1" "length 𝔏 - 1 > 0" "length 𝔏 - 1 ≤ length 𝔏" using n'(6) length by auto
      have Inteq𝔏sndlast: "ℌ ! (m - 1) ∩ 𝔊 ! (n - 1) = 𝔏 ! (length 𝔏 - 1 - 1)"
      proof -
        have "length 𝔏 - 1 - 1 + 1 < length 𝔏" using length𝔏' by auto
        moreover have KGnotempty: "(map ((∩) (𝔊 ! (n - 1))) ℌ) ≠ []" using compℌ.notempty by (metis Nil_is_map_conv)
        ultimately obtain i where i: "i + 1 < length (map ((∩) (𝔊 ! (n - 1))) ℌ)"
          "𝔏 ! (length 𝔏 - 1 - 1) = (map ((∩) (𝔊 ! (n - 1))) ℌ) ! i" "𝔏 ! (length 𝔏 - 1 - 1 + 1) = (map ((∩) (𝔊 ! (n - 1))) ℌ) ! (i + 1)"
          using remdups_adj_obtain_adjacency unfolding 𝔏_def by force
        hence "𝔏 ! (length 𝔏 - 1 - 1) = ℌ ! i ∩ 𝔊 ! (n - 1)" "𝔏 ! (length 𝔏 - 1 - 1 + 1) = ℌ ! (i + 1) ∩ 𝔊 ! (n - 1)" by auto
        hence "𝔏 ! (length 𝔏 - 1) = ℌ ! (i + 1) ∩ 𝔊 ! (n - 1)" using length𝔏'(2) by (metis Suc_diff_1 Suc_eq_plus1)
        hence 𝔊PnsubℌPm: "𝔊 ! (n - 1) ⊆ ℌ ! (i + 1)" using 𝔏.last 𝔏.notempty last_conv_nth unfolding 𝔊Pn_def by auto
        from i(1) have "i + 1 < m + 1" unfolding m_def by auto
        moreover have "¬ (i + 1 ≤ m - 1)" using compℌ.entries_mono m'(6) not𝔊PnSubℌPm 𝔊PnsubℌPm by fastforce
        ultimately have "m - 1 = i" by auto
        with i show ?thesis by auto
      qed
      hence 𝔏sndlast: "ℌPmInt𝔊Pn = (𝔊Pn⦇carrier := 𝔏 ! (length 𝔏 - 1 - 1)⦈)" unfolding ℌPmInt𝔊Pn_def 𝔊Pn_def by auto
      then interpret 𝔏butlast: composition_series ℌPmInt𝔊Pn "take (length 𝔏 - 1) 𝔏" using length𝔏' 𝔏.composition_series_prefix_closed by metis
      from ‹length 𝔏 > 1› have quots𝔏notemtpy: "𝔏.quotients ≠ []" unfolding 𝔏.quotients_def by auto

      ― ‹Apply the induction hypothesis on @{text 𝔏butlast} and @{text 𝔎butlast}›
      have "length 𝔎 > 1"
      proof (rule ccontr)
        assume "¬ length 𝔎 > 1"
        with 𝔎.notempty have "length 𝔎 = 1" by (metis One_nat_def Suc_lessI length_greater_0_conv)
        hence "carrier ℌPm = {𝟭⇘ℌPm⇙}" using 𝔎.composition_series_length_one 𝔎.composition_series_triv_group by auto
        hence "carrier ℌPm = {𝟭⇘G⇙}" unfolding ℌPm_def by auto
        hence "carrier ℌPm ⊆ 𝔊 ! (n - 1)" using 𝔊Pnmax.is_subgroup subgroup.one_closed by auto
        with notℌPmSub𝔊Pn show False unfolding ℌPm_def by auto
      qed
      hence length𝔎': "length 𝔎 - 1 > 0" "length 𝔎 - 1 ≤ length 𝔎" by auto 
      have Inteq𝔎sndlast: "ℌ ! (m - 1) ∩ 𝔊 ! (n - 1) = 𝔎 ! (length 𝔎 - 1 - 1)"
      proof -
        have "length 𝔎 - 1 - 1 + 1 < length 𝔎" using length𝔎' by auto
        moreover have KGnotempty: "(map ((∩) (ℌ ! (m - 1))) 𝔊) ≠ []" using comp𝔊.notempty by (metis Nil_is_map_conv)
        ultimately obtain i where i: "i + 1 < length (map ((∩) (ℌ ! (m - 1))) 𝔊)"
          "𝔎 ! (length 𝔎 - 1 - 1) = (map ((∩) (ℌ ! (m - 1))) 𝔊) ! i" "𝔎 ! (length 𝔎 - 1 - 1 + 1) = (map ((∩) (ℌ ! (m - 1))) 𝔊) ! (i + 1)"
          using remdups_adj_obtain_adjacency unfolding 𝔎_def by force
        hence "𝔎 ! (length 𝔎 - 1 - 1) = 𝔊 ! i ∩ ℌ ! (m - 1)" "𝔎 ! (length 𝔎 - 1 - 1 + 1) = 𝔊 ! (i + 1) ∩ ℌ ! (m - 1)" by auto
        hence "𝔎 ! (length 𝔎 - 1) = 𝔊 ! (i + 1) ∩ ℌ ! (m - 1)" using length𝔎'(1) by (metis Suc_diff_1 Suc_eq_plus1)
        hence ℌPmsub𝔊Pn: "ℌ ! (m - 1) ⊆ 𝔊 ! (i + 1)" using 𝔎.last 𝔎.notempty last_conv_nth unfolding ℌPm_def by auto
        from i(1) have "i + 1 < n + 1" unfolding n_def by auto
        moreover have "¬ (i + 1 ≤ n - 1)" using comp𝔊.entries_mono n'(2) notℌPmSub𝔊Pn ℌPmsub𝔊Pn by fastforce
        ultimately have "n - 1 = i" by auto
        with i show ?thesis by auto
      qed
      have "composition_series (G⦇carrier := 𝔎 ! (length 𝔎 - 1 - 1)⦈) (take (length 𝔎 - 1) 𝔎)"
        using length𝔎' 𝔎.composition_series_prefix_closed unfolding ℌPmInt𝔊Pn_def ℌPm_def by fastforce
      then interpret 𝔎butlast: composition_series ℌPmInt𝔊Pn "(take (length 𝔎 - 1) 𝔎)" using Inteq𝔎sndlast unfolding ℌPmInt𝔊Pn_def by auto
      from finGbl have finInt: "finite (carrier ℌPmInt𝔊Pn)" unfolding ℌPmInt𝔊Pn_def 𝔊Pn_def by simp
      moreover have "Suc (length (take (length 𝔏 - 1) 𝔏)) ≤ length 𝔊" using length𝔏 unfolding n_def using n'(2) by auto
      ultimately have multisets𝔎𝔏butlast: "mset (map group.iso_class 𝔏butlast.quotients) = mset (map group.iso_class 𝔎butlast.quotients)"
         using "1.hyps" 𝔏butlast.is_group 𝔎butlast.is_composition_series 𝔏butlast.is_composition_series by auto
      hence "length (take (length 𝔎 - 1) 𝔎) = length (take (length 𝔏 - 1) 𝔏)"
        using 𝔎butlast.quotients_length 𝔏butlast.quotients_length length_map size_mset by metis
      hence "length (take (length 𝔎 - 1) 𝔎) = n - 1" using length𝔏 n'(1) by auto
      hence length𝔎: "length 𝔎 = n" by (metis Suc_diff_1 𝔎.notempty butlast_conv_take length_butlast length_greater_0_conv n'(1))
      
      ― ‹Apply the induction hypothesis on @{text 𝔎} and @{text ℌbutlast}›
      from Inteq𝔎sndlast have 𝔎sndlast: "ℌPmInt𝔊Pn = (ℌPm⦇carrier := 𝔎 ! (length 𝔎 - 1 - 1)⦈)" unfolding ℌPmInt𝔊Pn_def ℌPm_def 𝔎_def by auto
      from length𝔎 have "Suc (length 𝔎) ≤ length 𝔊" using n'(2) by auto
      hence multisetsℌbutlast𝔎: "mset (map group.iso_class ℌbutlast.quotients) = mset (map group.iso_class 𝔎.quotients)"
        using  "1.hyps" grpℌPm.is_group finHbl ℌbutlast.is_composition_series 𝔎.is_composition_series by metis
      hence length𝔎: "m = length 𝔎" using ℌbutlast.quotients_length 𝔎.quotients_length length_map size_mset ltakem by metis
      hence  "length 𝔎 > 1" "length 𝔎 - 1 > 0" "length 𝔎 - 1 ≤ length 𝔎" using m'(4) lengthℌbig by auto
      hence quots𝔎notemtpy: "𝔎.quotients ≠ []" unfolding 𝔎.quotients_def by auto
      
      interpret 𝔎butlastadd𝔊Pn: composition_series 𝔊Pn "(take (length 𝔎 - 1) 𝔎) @ [𝔊 ! (n - 1)]"
        using grp𝔊Pn.composition_series_extend 𝔎butlast.is_composition_series simple𝔊PnModInt Intnorm𝔊Pn
        unfolding 𝔊Pn_def ℌPmInt𝔊Pn_def by auto
      interpret 𝔏butlastaddℌPm: composition_series ℌPm "(take (length 𝔏 - 1) 𝔏) @ [ℌ ! (m - 1)]"
        using grpℌPm.composition_series_extend 𝔏butlast.is_composition_series simpleℌPmModInt IntnormℌPm
        unfolding ℌPm_def ℌPmInt𝔊Pn_def by auto
      
      ― ‹Prove equality of those composition series.›
      have "mset (map group.iso_class comp𝔊.quotients)
                    = mset (map group.iso_class ((butlast comp𝔊.quotients) @ [last comp𝔊.quotients]))" using quots𝔊notempty by simp
      also have "… = mset (map group.iso_class (𝔊butlast.quotients @ [G Mod 𝔊 ! (n - 1)]))"
        using comp𝔊.quotients_butlast comp𝔊.last_quotient length unfolding n_def 𝔊Pn_def by auto
      also have "… = mset (map group.iso_class ((butlast 𝔏.quotients) @ [last 𝔏.quotients])) + {# group.iso_class (G Mod 𝔊 ! (n - 1)) #}"
        using multisets𝔊butlast𝔏 quots𝔏notemtpy by simp
      also have "… = mset (map group.iso_class (𝔏butlast.quotients @ [𝔊Pn Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)])) + {# group.iso_class (G Mod 𝔊 ! (n - 1)) #}"
        using 𝔏.quotients_butlast 𝔏.last_quotient ‹length 𝔏 > 1› 𝔏sndlast Inteq𝔏sndlast unfolding n_def by auto
      also have "… = mset (map group.iso_class 𝔎butlast.quotients) + {# group.iso_class (𝔊Pn Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)) #} + {# group.iso_class (G Mod 𝔊 ! (n - 1)) #}"
        using multisets𝔎𝔏butlast by simp
      also have "… = mset (map group.iso_class 𝔎butlast.quotients) + {# group.iso_class (G Mod ℌ ! (m - 1)) #} + {# group.iso_class (ℌPm Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)) #}"
        using φ ψ2 iso_classes_iff grp𝔊PnModℌPmint𝔊Pn.is_group grpGModℌPm.is_group grpGMod𝔊Pn.is_group grpℌPmModℌPmint𝔊Pn.is_group
        by metis
      also have "… = mset (map group.iso_class 𝔎butlast.quotients) + {# group.iso_class (ℌPm Mod ℌ ! (m - 1) ∩ 𝔊 ! (n - 1)) #} + {# group.iso_class (G Mod ℌ ! (m - 1)) #}"
        by simp
      also have "… = mset (map group.iso_class ((butlast 𝔎.quotients) @ [last 𝔎.quotients])) + {# group.iso_class (G Mod ℌ ! (m - 1)) #}"
        using 𝔎.quotients_butlast 𝔎.last_quotient ‹length 𝔎 > 1› 𝔎sndlast Inteq𝔎sndlast unfolding m_def by auto
      also have "… = mset (map group.iso_class ℌbutlast.quotients) + {# group.iso_class (G Mod ℌ ! (m - 1)) #}"
        using multisetsℌbutlast𝔎 quots𝔎notemtpy by simp
      also have "… = mset (map group.iso_class ((butlast compℌ.quotients) @ [last compℌ.quotients]))"
        using compℌ.quotients_butlast compℌ.last_quotient lengthℌbig unfolding m_def ℌPm_def by auto
      also have "… = mset (map group.iso_class compℌ.quotients)" using quotsℌnotempty by simp
      finally show ?thesis .
    qed
  qed
qed

text ‹As a corollary, we see that the composition series of a fixed group all have the same length.›

corollary (in jordan_hoelder) jordan_hoelder_size:
  shows "length 𝔊 = length ℌ"
proof -
  have "length 𝔊 = length comp𝔊.quotients + 1" by (metis comp𝔊.quotients_length)
  also have "… = size (mset (map group.iso_class comp𝔊.quotients)) + 1" by (metis length_map size_mset)
  also have "… = size (mset (map group.iso_class compℌ.quotients)) + 1"
    using jordan_hoelder_multisets is_group finite is_composition_series compℌ.is_composition_series by metis
  also have "… = length compℌ.quotients + 1" by (metis size_mset length_map)
  also have "… = length ℌ" by (metis compℌ.quotients_length)
  finally show ?thesis.
qed

end