Quelle  Product_Groups.thy

(*  Title:      HOL/Algebra/Product_Groups.thy
  Author: LC Paulson (ported from HOL Light)
*)

section ‹Product and Sum Groups›

theory Product_Groups
  imports Elementary_Groups "HOL-Library.Equipollence" 
  
begin

subsection ‹Product of a Family of Groups›

definition product_group:: "'a set ==> ('a ==> ('b, 'c) monoid_scheme) ==> ('a ==> 'b) monoid"
  where "product_group I G ≡ (carrier = (Π🪙E i∈I. carrier (G i)),
                              monoid.mult = (λx y. (λi∈I. x i ⊗🪙G i🪙 y i)),
                              one = (λi∈I. 1🪙G i🪙))"

lemma carrier_product_group [simp]: "carrier(product_group I G) = (Π🪙E i∈I. carrier (G i))"
  by (simp add: product_group_def)

lemma one_product_group [simp]: "one(product_group I G) = (λi∈I. one (G i))"
  by (simp add: product_group_def)

lemma mult_product_group [simp]: "(⊗🪙product_group I G🪙) = (λx y. λi∈I. x i ⊗🪙G i?? y i)"
  by (simp add: product_group_def)

lemma product_group [simp]:
  assumes "∧i. i ∈ I ==> group (G i)" shows "group (product_group I G)"
proof (rule groupI; simp)
  show "(λi. x i ⊗🪙G i🪙 y i) ∈ (Π i∈I. carrier (G i))"
    if "x ∈ (Π🪙E i∈I. carrier (G i))" "y ∈ (Π🪙E i∈I. carrier (G i))" for x y
    using that assms group.subgroup_self subgroup.m_closed by fastforce
  show "(λi. 1🪙G i🪙) ∈ (Π i∈I. carrier (G i))"
    by (simp add: assms group.is_monoid)
  show "(λi∈I. (if i ∈ I then x i ⊗🪙G i🪙 y i else undefined) ⊗🪙G i🪙 z i) =
        (λi∈I. x i ⊗🪙G i🪙 (if i ∈ I then y i ⊗🪙G i🪙 z i else undefined))"
    if "x ∈ (Π🪙E i∈I. carrier (G i))" "y ∈ (Π🪙E i∈I. carrier (G i))" "z ∈ (Π🪙E i∈I. carrier (G i))" for x y z
    using that  by (auto simp: PiE_iff assms group.is_monoid monoid.m_assoc intro: restrict_ext)
  show "(λi∈I. (if i ∈ I then 1🪙G i🪙 else undefined) ⊗🪙G i🪙 x i) = x"
    if "x ∈ (Π🪙E i∈I. carrier (G i))" for x
    using assms that by (fastforce simp: Group.group_def PiE_iff)
  show "∃y∈Π🪙E i∈I. carrier (G i). (λi∈I. y i ⊗🪙G i🪙 x i) = (λi∈I. 1🪙G i🪙)"
    if "x ∈ (Π🪙E i∈I. carrier (G i))" for x
    by (rule_tac x="λi∈I. inv🪙G i🪙 x i" in bexI) (use assms that in ‹auto simp: PiE_iff group.l_inv›)
qed

lemma inv_product_group [simp]:
  assumes "f ∈ (Π🪙E i∈I. carrier (G i))" "∧i. i ∈ I ==> group (G i)"
  shows "inv🪙product_group I G🪙 f = (λi∈I. inv🪙G i🪙 f i)"
proof (rule group.inv_equality)
  show "Group.group (product_group I G)"
    by (simp add: assms)
  show "(λi∈I. inv🪙G i🪙 f i) ⊗🪙product_group I G🪙 f = 1🪙product_group I G🪙"
    using assms by (auto simp: PiE_iff group.l_inv)
  show "f ∈ carrier (product_group I G)"
    using assms by simp
  show "(λi∈I. inv🪙G i🪙 f i) ∈ carrier (product_group I G)"
    using PiE_mem assms by fastforce
qed


lemma trivial_product_group: "trivial_group(product_group I G) ⟷ (∀i ∈ I. trivial_group(G i))"
 (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have "inv🪙product_group I G🪙 (λa∈I. 1🪙G a🪙) = 1🪙product_group I G🪙"
    by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
  have [simp]: "1🪙G i🪙 ⊗🪙G i🪙 1🪙G i🪙 = 1🪙G i🪙" if "i ∈ I" for i
    unfolding trivial_group_def
  proof -
    have 1: "(λa∈I. 1🪙G a🪙) i = 1🪙G i🪙"
      by (simp add: that)
    have "(λa∈I. 1🪙G a🪙) = (λa∈I. 1🪙G a🪙) ⊗🪙product_group I G🪙 (λa∈I. 1🪙G a🪙)"
      by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def)
    then show ?thesis
      using 1 by (simp add: that)
  qed
  show ?rhs
    using L
    by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI)
next
  assume ?rhs
  then show ?lhs
    by (simp add: PiE_eq_singleton trivial_group_def)
qed


lemma PiE_subgroup_product_group:
  assumes "∧i. i ∈ I ==> group (G i)"
  shows "subgroup (PiE I H) (product_group I G) ⟷ (∀i ∈ I. subgroup (H i) (G i))"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have [simp]: "PiE I H ≠ {}"
    using subgroup_nonempty by force
  show ?rhs
  proof (clarify; unfold_locales)
    show sub: "H i ⊆ carrier (G i)" if "i ∈ I" for i
      using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE)
    show "x ⊗🪙G i🪙 y ∈ H i" if "i ∈ I" "x ∈ H i" "y ∈ H i" for i x y
    proof -
      have *: "∧x. x ∈ Pi🪙E I H ==> (∀y ∈ Pi🪙E I H. ∀i∈I. x i ⊗🪙G i🪙 y i ∈ H i)"
        using L by (auto simp: subgroup_def Pi_iff)
      have "∀y∈H i. f i ⊗🪙G i🪙 y ∈ H i" if f: "f ∈ Pi🪙E I H" and "i ∈ I" for i f
        using * [OF f] ‹i ∈ I›
        by (subst(asm) all_PiE_elements) auto
      then have "∀f ∈ Pi🪙E I H. ∀i ∈ I. ∀y∈H i. f i ⊗🪙G i🪙 y ∈ H i"
        by blast
      with that show ?thesis
        by (subst(asm) all_PiE_elements) auto
    qed
    show "1🪙G i🪙 ∈ H i" if "i ∈ I" for i
      using L subgroup.one_closed that by fastforce
    show "inv🪙G i🪙 x ∈ H i" if "i ∈ I" and x: "x ∈ H i" for i x
    proof -
      have *: "∀y ∈ Pi🪙E I H. ∀i∈I. inv🪙G i🪙 y i ∈ H i"
      proof
        fix y
        assume y: "y ∈ Pi🪙E I H"
        then have yc: "y ∈ carrier (product_group I G)"
          by (metis (no_types) L subgroup_def subsetCE)
        have "inv🪙product_group I G🪙 y ∈ Pi🪙E I H"
          by (simp add: y L subgroup.m_inv_closed)
        moreover have "inv🪙product_group I G🪙 y = (λi∈I. inv🪙G i🪙 y i)"
          using yc by (simp add: assms)
        ultimately show "∀i∈I. inv🪙G i🪙 y i ∈ H i"
          by auto
      qed
      then have "∀i∈I. ∀x∈H i. inv🪙G i🪙 x ∈ H i"
        by (subst(asm) all_PiE_elements) auto
      then show ?thesis
        using that(1) x by blast
    qed
  qed
next
  assume R: ?rhs
  show ?lhs
  proof
    show "Pi🪙E I H ⊆ carrier (product_group I G)"
      using R by (force simp: subgroup_def)
    show "x ⊗🪙product_group I G🪙 y ∈ Pi🪙E I H" if "x ∈ Pi🪙E I H" "y ∈ Pi🪙E I H" for x y
      using R that by (auto simp: PiE_iff subgroup_def)
    show "1🪙product_group I G🪙 ∈ Pi🪙E I H"
      using R by (force simp: subgroup_def)
    show "inv🪙product_group I G🪙 x ∈ Pi🪙E I H" if "x ∈ Pi🪙E I H" for x
    proof -
      have x: "x ∈ (Π🪙E i∈I. carrier (G i))"
        using R that by (force simp:  subgroup_def)
      show ?thesis
        using assms R that by (fastforce simp: x assms subgroup_def)
    qed
  qed
qed

lemma product_group_subgroup_generated:
  assumes "∧i. i ∈ I ==> subgroup (H i) (G i)" and gp: "∧i. i ∈ I ==> group (G i)"
  shows "product_group I (λi. subgroup_generated (G i) (H i))
       = subgroup_generated (product_group I G) (PiE I H)"
proof (rule monoid.equality)
  have [simp]: "∧i. i ∈ I ==> carrier (G i) ∩ H i = H i" "(Π🪙E i∈I. carrier (G i)) ∩ Pi🪙E I H = Pi🪙E I H"
    using assms by (force simp: subgroup_def)+
  have "(Π🪙E i∈I. generate (G i) (H i)) = generate (product_group I G) (Pi🪙E I H)"
  proof (rule group.generateI)
    show "Group.group (product_group I G)"
      using assms by simp
    show "subgroup (Π🪙E i∈I. generate (G i) (H i)) (product_group I G)"
      using assms by (simp add: PiE_subgroup_product_group group.generate_is_subgroup subgroup.subset)
    show "Pi🪙E I H ⊆ (Π🪙E i∈I. generate (G i) (H i))"
      using assms by (auto simp: PiE_iff generate.incl)
    show "(Π🪙E i∈I. generate (G i) (H i)) ⊆ K"
      if "subgroup K (product_group I G)" "Pi🪙E I H ⊆ K" for K
      using assms that group.generate_subgroup_incl by fastforce
  qed
  with assms
  show "carrier (product_group I (λi. subgroup_generated (G i) (H i))) =
        carrier (subgroup_generated (product_group I G) (Pi🪙E I H))"
    by (simp add: carrier_subgroup_generated cong: PiE_cong)
qed auto

lemma finite_product_group:
  assumes "∧i. i ∈ I ==> group (G i)"
  shows
   "finite (carrier (product_group I G)) ⟷
    finite {i. i ∈ I ∧ ~ trivial_group(G i)} ∧ (∀i ∈ I. finite(carrier(G i)))"
proof -
  have [simp]: "∧i. i ∈ I ==> carrier (G i) ≠ {}"
    using assms group.is_monoid by blast
  show ?thesis
    by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong)
qed

subsection ‹Sum of a Family of Groups›

definition sum_group :: "'a set ==> ('a ==> ('b, 'c) monoid_scheme) ==> ('a ==> 'b) monoid"
  where "sum_group I G ≡
        subgroup_generated
         (product_group I G)
         {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"

lemma subgroup_sum_group:
  assumes "∧i. i ∈ I ==> group (G i)"
  shows "subgroup {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}
                  (product_group I G)"
proof unfold_locales
  fix x y
  have *: "{i. (i ∈ I ⟶ x i ⊗🪙G i🪙 y i ≠ 1🪙G i🪙) ∧ i ∈ I}
        ⊆ {i ∈ I. x i ≠ 1🪙G i🪙} ∪ {i ∈ I. y i ≠ 1🪙G i🪙}"
    by (auto simp: Group.group_def dest: assms)
  assume
    "x ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
    "y ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
  then
  show "x ⊗🪙product_group I G🪙 y ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
    using assms
    apply (auto simp: Group.group_def monoid.m_closed PiE_iff)
    apply (rule finite_subset [OF *])
    by blast
next
  fix x
  assume "x ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
  then show "inv🪙product_group I G🪙 x ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
    using assms
    by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong)
qed (use assms [unfolded Group.group_def] in auto)

lemma carrier_sum_group:
  assumes "∧i. i ∈ I ==> group (G i)"
  shows "carrier(sum_group I G) = {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
proof -
  interpret SG: subgroup "{x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}" "(product_group I G)"
    by (simp add: assms subgroup_sum_group)
  show ?thesis
    by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt)
qed

lemma one_sum_group [simp]: "1🪙sum_group I G🪙 = (λi∈I. 1🪙G i🪙)"
  by (simp add: sum_group_def)

lemma mult_sum_group [simp]: "(⊗🪙sum_group I G🪙) = (λx y. (λi∈I. x i ⊗🪙G i🪙 y i))"
  by (auto simp: sum_group_def)

lemma sum_group [simp]:
  assumes "∧i. i ∈ I ==> group (G i)" shows "group (sum_group I G)"
proof (rule groupI)
  note group.is_monoid [OF assms, simp]
  show "x ⊗🪙sum_group I G🪙 y ∈ carrier (sum_group I G)"
    if "x ∈ carrier (sum_group I G)" and
      "y ∈ carrier (sum_group I G)" for x y
  proof -
    have *: "{i ∈ I. x i ⊗🪙G i🪙 y i ≠ 1🪙G i🪙} ⊆ {i ∈ I. x i ≠ 1🪙G i🪙} ∪ {i ∈ I. y i ≠ 1🪙G i🪙}"
      by auto
    show ?thesis
      using that
      apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong)
      apply (blast intro: finite_subset [OF *])
      done
  qed
  show "1🪙sum_group I G🪙 ⊗🪙sum_group I G🪙 x = x"
    if "x ∈ carrier (sum_group I G)" for x
    using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def)
  show "∃y∈carrier (sum_group I G). y ⊗🪙sum_group I G🪙 x = 1🪙sum_group I G🪙"
    if "x ∈ carrier (sum_group I G)" for x
  proof
    let ?y = "λi∈I. m_inv (G i) (x i)"
    show "?y ⊗🪙sum_group I G🪙 x = 1🪙sum_group I G🪙"
      using that assms
      by (auto simp: carrier_sum_group PiE_iff group.l_inv)
    show "?y ∈ carrier (sum_group I G)"
      using that assms
      by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong)
  qed
qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc)

lemma inv_sum_group [simp]:
  assumes "∧i. i ∈ I ==> group (G i)" and x: "x ∈ carrier (sum_group I G)"
  shows "m_inv (sum_group I G) x = (λi∈I. m_inv (G i) (x i))"
proof (rule group.inv_equality)
  show "(λi∈I. inv🪙G i🪙 x i) ⊗🪙sum_group I G🪙 x = 1🪙sum_group I G🪙"
    using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
  show "(λi∈I. inv🪙G i🪙 x i) ∈ carrier (sum_group I G)"
    using x by (simp add: carrier_sum_group PiE_iff group.inv_eq_1_iff assms conj_commute cong: rev_conj_cong)
qed (auto simp: assms)


thm group.subgroups_Inter (*REPLACE*)
theorem subgroup_Inter:
  assumes subgr: "(∧H. H ∈ A ==> subgroup H G)"
    and not_empty: "A ≠ {}"
  shows "subgroup (∩A) G"
proof
  show "∩ A ⊆ carrier G"
    by (simp add: Inf_less_eq not_empty subgr subgroup.subset)
qed (auto simp: subgr subgroup.m_closed subgroup.one_closed subgroup.m_inv_closed)

thm group.subgroups_Inter_pair (*REPLACE*)
lemma subgroup_Int:
  assumes "subgroup I G" "subgroup J G"
  shows "subgroup (I ∩ J) G" using subgroup_Inter[ where ?A = "{I,J}"] assms by auto


lemma sum_group_subgroup_generated:
  assumes "∧i. i ∈ I ==> group (G i)" and sg: "∧i. i ∈ I ==> subgroup (H i) (G i)"
  shows "sum_group I (λi. subgroup_generated (G i) (H i)) = subgroup_generated (sum_group I G) (PiE I H)"
proof (rule monoid.equality)
  have "subgroup (carrier (sum_group I G) ∩ Pi🪙E I H) (product_group I G)"
    by (rule subgroup_Int) (auto simp: assms carrier_sum_group subgroup_sum_group PiE_subgroup_product_group)
  moreover have "carrier (sum_group I G) ∩ Pi🪙E I H
              ⊆ carrier (subgroup_generated (product_group I G)
                    {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}})"
    by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
  ultimately
  have "subgroup (carrier (sum_group I G) ∩ Pi🪙E I H) (sum_group I G)"
    by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
  then have *: "{f ∈ Π🪙E i∈I. carrier (subgroup_generated (G i) (H i)). finite {i ∈ I. f i ≠ 1🪙G i🪙}}
      = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) ∩ Pi🪙E I H))"
    apply (simp only: subgroup.carrier_subgroup_generated_subgroup)
    using subgroup.subset [OF sg]
    apply (auto simp: set_eq_iff PiE_def Pi_def assms carrier_sum_group subgroup.carrier_subgroup_generated_subgroup)
    done
  then show "carrier (sum_group I (λi. subgroup_generated (G i) (H i))) =
        carrier (subgroup_generated (sum_group I G) (Pi🪙E I H))"
    by simp (simp add: assms group.subgroupE(1) group.group_subgroup_generated carrier_sum_group)
qed (auto simp: sum_group_def subgroup_generated_def)


lemma iso_product_groupI:
  assumes iso: "∧i. i ∈ I ==> G i ≅ H i"
    and G: "∧i. i ∈ I ==> group (G i)" and H: "∧i. i ∈ I ==> group (H i)"
  shows "product_group I G ≅ product_group I H" (is "?IG ≅ ?IH")
proof -
  have "∧i. i ∈ I ==> ∃h. h ∈ iso (G i) (H i)"
    using iso by (auto simp: is_iso_def)
  then obtain f where f: "∧i. i ∈ I ==> f i ∈ iso (G i) (H i)"
    by metis
  define h where "h ≡ λx. (λi∈I. f i (x i))"
  have hom: "h ∈ iso ?IG ?IH"
  proof (rule isoI)
    show hom: "h ∈ hom ?IG ?IH"
    proof (rule homI)
      fix x
      assume "x ∈ carrier ?IG"
      with f show "h x ∈ carrier ?IH"
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def)
    next
      fix x y
      assume "x ∈ carrier ?IG" "y ∈ carrier ?IG"
      with f show "h (x ⊗🪙?IG🪙 y) = h x ⊗🪙?IH🪙 h y"
        apply (simp add: h_def PiE_def iso_def hom_def)
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def intro: restrict_ext)
    qed
    with G H interpret GH : group_hom "?IG" "?IH" h
      by (simp add: group_hom_def group_hom_axioms_def)
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
      unfolding bij_betw_def
    proof (intro conjI subset_antisym)
      have "γ i = 1🪙G i🪙"
        if γ: "γ ∈ (Π🪙E i∈I. carrier (G i))" and eq: "(λi∈I. f i (γ i)) = (λi∈I. 1🪙H i🪙)" and "i ∈ I"
        for γ i
      proof -
        have "inj_on (f i) (carrier (G i))" "f i ∈ hom (G i) (H i)"
          using ‹i ∈ I› f by (auto simp: iso_def bij_betw_def)
        then have *: "∧x. [f i x = 1🪙H i🪙; x ∈ carrier (G i)] ==> x = 1🪙G i🪙"
          by (metis G Group.group_def H hom_one inj_onD monoid.one_closed ‹i ∈ I›)
        show ?thesis
          using eq ‹i ∈ I› * γ by (simp add: fun_eq_iff) (meson PiE_iff)
      qed
      then show "inj_on h (carrier ?IG)"
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group)
        apply (force simp: h_def)
        done
    next
      show "h ` carrier ?IG ⊆ carrier ?IH"
        unfolding h_def using f
        by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE)
    next
      show "carrier ?IH ⊆ h ` carrier ?IG"
        unfolding h_def
      proof (clarsimp simp: iso_def bij_betw_def)
        fix x
        assume "x ∈ (Π🪙E i∈I. carrier (H i))"
        with f have x: "x ∈ (Π🪙E i∈I. f i ` carrier (G i))"
          unfolding h_def by (auto simp: iso_def bij_betw_def)
        have "∧i. i ∈ I ==> inj_on (f i) (carrier (G i))"
          using f by (auto simp: iso_def bij_betw_def)
        let ?g = "λi∈I. inv_into (carrier (G i)) (f i) (x i)"
        show "x ∈ (λg. λi∈I. f i (g i)) ` (Π🪙E i∈I. carrier (G i))"
        proof
          show "x = (λi∈I. f i (?g i))"
            using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f)
          show "?g ∈ (Π🪙E i∈I. carrier (G i))"
            using x by (auto simp: PiE_iff inv_into_into)
        qed
      qed
    qed
  qed
  then show ?thesis
    using is_iso_def by auto
qed

lemma iso_sum_groupI:
  assumes iso: "∧i. i ∈ I ==> G i ≅ H i"
    and G: "∧i. i ∈ I ==> group (G i)" and H: "∧i. i ∈ I ==> group (H i)"
  shows "sum_group I G ≅ sum_group I H" (is "?IG ≅ ?IH")
proof -
  have "∧i. i ∈ I ==> ∃h. h ∈ iso (G i) (H i)"
    using iso by (auto simp: is_iso_def)
  then obtain f where f: "∧i. i ∈ I ==> f i ∈ iso (G i) (H i)"
    by metis
  then have injf: "inj_on (f i) (carrier (G i))"
    and homf: "f i ∈ hom (G i) (H i)" if "i ∈ I" for i
    using ‹i ∈ I› f by (auto simp: iso_def bij_betw_def)
  then have one: "∧x. [f i x = 1🪙H i🪙; x ∈ carrier (G i)] ==> x = 1🪙G i🪙" if "i ∈ I" for i
    by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that)
  have fin1: "finite {i ∈ I. x i ≠ 1🪙G i🪙} ==> finite {i ∈ I. f i (x i) ≠ 1🪙H i🪙}" for x
    using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
  define h where "h ≡ λx. (λi∈I. f i (x i))"
  have hom: "h ∈ iso ?IG ?IH"
  proof (rule isoI)
    show hom: "h ∈ hom ?IG ?IH"
    proof (rule homI)
      fix x
      assume "x ∈ carrier ?IG"
      with f fin1 show "h x ∈ carrier ?IH"
        by (force simp: h_def PiE_def iso_def hom_def carrier_sum_group assms conj_commute cong: conj_cong)
    next
      fix x y
      assume "x ∈ carrier ?IG" "y ∈ carrier ?IG"
      with homf show "h (x ⊗🪙?IG🪙 y) = h x ⊗🪙?IH🪙 h y"
        by (fastforce simp add: h_def PiE_def hom_def carrier_sum_group assms intro: restrict_ext)
    qed
    with G H interpret GH : group_hom "?IG" "?IH" h
      by (simp add: group_hom_def group_hom_axioms_def)
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
      unfolding bij_betw_def
    proof (intro conjI subset_antisym)
      have γ: "γ i = 1🪙G i🪙"
        if "γ ∈ (Π🪙E i∈I. carrier (G i))" and eq: "(λi∈I. f i (γ i)) = (λi∈I. 1🪙H i🪙)" and "i ∈ I"
        for γ i
        using ‹i ∈ I› one that by (simp add: fun_eq_iff) (meson PiE_iff)
      show "inj_on h (carrier ?IG)"
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group)
        apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one)
        done
    next
      show "h ` carrier ?IG ⊆ carrier ?IH"
        using homf GH.hom_closed
        by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE)
    next
      show "carrier ?IH ⊆ h ` carrier ?IG"
        unfolding h_def
      proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms)
        fix x
        assume x: "x ∈ (Π🪙E i∈I. carrier (H i))" and fin: "finite {i ∈ I. x i ≠ 1🪙H i🪙}"
        with f have xf: "x ∈ (Π🪙E i∈I. f i ` carrier (G i))"
          unfolding h_def
          by (auto simp: iso_def bij_betw_def)
        have "∧i. i ∈ I ==> inj_on (f i) (carrier (G i))"
          using f by (auto simp: iso_def bij_betw_def)
        let ?g = "λi∈I. inv_into (carrier (G i)) (f i) (x i)"
        show "x ∈ (λg. λi∈I. f i (g i))
                 ` {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
        proof
          show xeq: "x = (λi∈I. f i (?g i))"
            using x by (clarsimp simp: PiE_iff fun_eq_iff extensional_def) (metis iso_iff f_inv_into_f f)
          have "finite {i ∈ I. inv_into (carrier (G i)) (f i) (x i) ≠ 1🪙G i🪙}"
            apply (rule finite_subset [OF _ fin])
            using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
          with x show "?g ∈ {x ∈ Π🪙E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 1🪙G i🪙}}"
            apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
            by (metis (no_types, opaque_lifting) iso_iff f inv_into_into)
        qed
      qed
    qed
  qed
  then show ?thesis
    using is_iso_def by auto
qed

end